Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/obtain.ML
changeset 11021 41de937d338b
parent 10582 49ebade930ea
child 11764 fd780dd6e0b4 
--- a/src/Pure/Isar/obtain.ML	Thu Feb 01 20:44:19 2001 +0100
+++ b/src/Pure/Isar/obtain.ML	Thu Feb 01 20:45:11 2001 +0100
@@ -11,7 +11,7 @@
 
   {
     fix thesis
-    assume that: "!!x. P x ==> thesis"
+    assume that [intro]: "!!x. P x ==> thesis"
     <chain_facts> have thesis <proof (insert that)>
   }
   fix x assm (obtained) "P x"
isabelle