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.
ThmDeps.enable;
authorwenzelm
Sun, 30 Jul 2000 12:50:33 +0200
changeset 9462 3ac87f80186d
parent 9461 8645b0413366
child 9463 4362bf779182
ThmDeps.enable;
src/Pure/Interface/proof_general.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Interface/proof_general.ML	Sun Jul 30 12:50:07 2000 +0200
+++ b/src/Pure/Interface/proof_general.ML	Sun Jul 30 12:50:33 2000 +0200
@@ -206,7 +206,7 @@
 
 local structure P = OuterParse and K = OuterSyntax.Keyword in
 
-val old_undoP =	(* FIXME same name for compatibility with PG/Isabelle99 *)
+val old_undoP = (* FIXME same name for compatibility with PG/Isabelle99 *)
   OuterSyntax.improper_command "undo" "undo last command (no output)" K.control
     (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
 
@@ -258,7 +258,9 @@
   setup_thy_loader ();
   print_mode := [proof_generalN];
   set quick_and_dirty;
-  ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373");
+  ThmDeps.enable ();
+  if isar then ml_prompts "ML> " "ML# "
+  else ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373");
   if isar then Isar.sync_main () else isa_restart ());
isabelle