Renamed file

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