Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
no begin_goal marker (interferes with "latex" etc. output; useless anyway?)
authorwenzelm
Fri, 17 Mar 2000 16:27:28 +0100
changeset 8495 4f5a3272c8ba
parent 8494 21074180a6f2
child 8496 7e4a466b18d5
no begin_goal marker (interferes with "latex" etc. output; useless anyway?)
src/Pure/Interface/proof_general.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Interface/proof_general.ML	Fri Mar 17 16:26:43 2000 +0100
+++ b/src/Pure/Interface/proof_general.ML	Fri Mar 17 16:27:28 2000 +0100
@@ -112,8 +112,7 @@
     let
       val begin_state = oct_char "366";
       val end_state= oct_char "367";
-      val begin_goal = oct_char "370";
-    in (begin_state, end_state, begin_goal) end;
+    in (begin_state, end_state, "") end;
   Toplevel.print_state_fn := plain_writeln Toplevel.print_state_default;
   Toplevel.prompt_state_fn := (suffix (oct_char "372") o Toplevel.prompt_state_default);
   Goals.print_current_goals_fn := print_current_goals);
isabelle