diff options
| -rw-r--r-- | isa/ProofGeneral.ML (renamed from isa/isa-print-functions.ML) | 17 |
1 files changed, 12 insertions, 5 deletions
diff --git a/isa/isa-print-functions.ML b/isa/ProofGeneral.ML index 3af539a5..bd0ccc3e 100644 --- a/isa/isa-print-functions.ML +++ b/isa/ProofGeneral.ML @@ -1,15 +1,13 @@ (* - isa-print-functions.ML + ProofGeneral.ML - Customized version of Isabelle printing for script management - mode. + Isabelle configuration for Proof General. $Id$ *) - val proof_state_special_prefix="\248"; val proof_state_special_suffix="\249"; val goal_start_special="\253"; @@ -167,6 +165,15 @@ end +(* Some top-level commands for Proof General. + These could easily be customized to do different things. +*) +structure ProofGeneral = + struct + fun kill_goal () = Goal "PROP no_goal_supplied"; + fun help () = print version; + fun show_context () = the_context(); + end; -
\ No newline at end of file +
\ No newline at end of file |