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.
isolate change of Proofterm.proofs in TPTP.thy from rest of session;
authorwenzelm
Wed, 23 Mar 2011 20:57:37 +0100
changeset 42078 d5bf0ce40bd7
parent 42077 96c50a4210a2
child 42079 71662f36b573
isolate change of Proofterm.proofs in TPTP.thy from rest of session; qualified Proofterm.proofs to facilitate grepping;
src/HOL/ex/ROOT.ML file | annotate | diff | comparison | revisions
src/HOL/ex/TPTP.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/ex/ROOT.ML	Wed Mar 23 20:51:36 2011 +0100
+++ b/src/HOL/ex/ROOT.ML	Wed Mar 23 20:57:37 2011 +0100
@@ -73,10 +73,12 @@
   "Quicksort",
   "Birthday_Paradoxon",
   "List_to_Set_Comprehension_Examples",
-  "Set_Algebras",
-  "TPTP"
+  "Set_Algebras"
 ];
 
+Unsynchronized.setmp Proofterm.proofs (! Proofterm.proofs)
+  use_thy "TPTP";
+
 if getenv "ISABELLE_GHC" = "" then ()
 else use_thy "Quickcheck_Narrowing_Examples";
 
--- a/src/HOL/ex/TPTP.thy	Wed Mar 23 20:51:36 2011 +0100
+++ b/src/HOL/ex/TPTP.thy	Wed Mar 23 20:57:37 2011 +0100
@@ -14,7 +14,7 @@
 
 declare [[smt_oracle]]
 
-ML {* proofs := 0 *}
+ML {* Proofterm.proofs := 0 *}
 
 ML {*
 fun SOLVE_TIMEOUT seconds name tac st =
isabelle