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.
Theory.checkpoint before commencing proof;
authorwenzelm
Thu, 11 Dec 2008 10:41:37 +0100
changeset 29057 d219318fd89a
parent 29056 dc08e3990c77
child 29058 c7c0dd65159a
Theory.checkpoint before commencing proof;
src/HOL/Tools/typedef_package.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/typedef_package.ML	Thu Dec 11 00:42:52 2008 +0100
+++ b/src/HOL/Tools/typedef_package.ML	Thu Dec 11 10:41:37 2008 +0100
@@ -108,6 +108,7 @@
         thy
         |> Sign.add_consts_i [(name, setT', NoSyn)]
         |> PureThy.add_defs false [Thm.no_attributes (PrimitiveDefs.mk_defpair (setC, set))]
+        ||> Theory.checkpoint
         |-> (fn [th] => pair (SOME th))
       else (NONE, thy);
isabelle