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.
Present.theorem;
authorwenzelm
Tue, 09 Mar 1999 12:17:40 +0100
changeset 6327 c6abb5884fed
parent 6326 1b55802e2b59
child 6328 dc72cf821659
Present.theorem;
src/Pure/Thy/thm_database.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Thy/thm_database.ML	Tue Mar 09 12:13:58 1999 +0100
+++ b/src/Pure/Thy/thm_database.ML	Tue Mar 09 12:17:40 1999 +0100
@@ -36,7 +36,7 @@
 
 fun store_thm (name, thm) =
   let val thm' = PureThy.smart_store_thm (name, thm)
-  in Present.thm name thm'; thm' end;
+  in Present.theorem name thm'; thm' end;
 
 
 (* store on ML toplevel *)
isabelle