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.
show/thus: Toplevel.proof';
authorwenzelm
Thu, 18 Jan 2001 20:38:58 +0100
changeset 10934 6ef388cedd58
parent 10933 0b3997a180dd
child 10935 808e9dbc68c4
show/thus: Toplevel.proof';
src/Pure/Isar/isar_syn.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/isar_syn.ML	Thu Jan 18 20:38:32 2001 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Thu Jan 18 20:38:58 2001 +0100
@@ -295,7 +295,7 @@
 
 val showP =
   OuterSyntax.command "show" "state local goal, solving current obligation" K.prf_goal
-    (statement IsarThy.show >> (fn f => Toplevel.print o Toplevel.proof f));
+    (statement IsarThy.show >> (fn f => Toplevel.print o Toplevel.proof' f));
 
 val haveP =
   OuterSyntax.command "have" "state local goal" K.prf_goal
@@ -303,7 +303,7 @@
 
 val thusP =
   OuterSyntax.command "thus" "abbreviates \"then show\"" K.prf_goal
-    (statement IsarThy.thus >> (fn f => Toplevel.print o Toplevel.proof f));
+    (statement IsarThy.thus >> (fn f => Toplevel.print o Toplevel.proof' f));
 
 val henceP =
   OuterSyntax.command "hence" "abbreviates \"then have\"" K.prf_goal
isabelle