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.
added @{clasimpset};
authorwenzelm
Sat, 20 Jan 2007 14:09:11 +0100
changeset 22128 cdd92316dd31
parent 22127 025dfa637f78
child 22129 bb2203c93316
added @{clasimpset};
src/FOL/simpdata.ML file | annotate | diff | comparison | revisions
src/HOL/simpdata.ML file | annotate | diff | comparison | revisions 
--- a/src/FOL/simpdata.ML	Sat Jan 20 14:09:10 2007 +0100
+++ b/src/FOL/simpdata.ML	Sat Jan 20 14:09:11 2007 +0100
@@ -342,4 +342,7 @@
   val iffD1 = iffD1 val iffD2 = iffD2 val notE = notE);
 open Clasimp;
 
+ML_Context.value_antiq "clasimpset"
+  (Scan.succeed ("clasimpset", "Clasimp.local_clasimpset_of (ML_Context.the_local_context ())"));
+
 val FOL_css = (FOL_cs, FOL_ss);
--- a/src/HOL/simpdata.ML	Sat Jan 20 14:09:10 2007 +0100
+++ b/src/HOL/simpdata.ML	Sat Jan 20 14:09:11 2007 +0100
@@ -177,9 +177,12 @@
 structure Clasimp = ClasimpFun
  (structure Simplifier = Simplifier and Splitter = Splitter
   and Classical  = Classical and Blast = Blast
-  val iffD1 = thm "iffD1" val iffD2 = thm "iffD2" val notE = thm "notE")
+  val iffD1 = thm "iffD1" val iffD2 = thm "iffD2" val notE = thm "notE");
 open Clasimp;
 
+val _ = ML_Context.value_antiq "clasimpset"
+  (Scan.succeed ("clasimpset", "Clasimp.local_clasimpset_of (ML_Context.the_local_context ())"));
+
 val mksimps_pairs =
   [("op -->", [thm "mp"]), ("op &", [thm "conjunct1", thm "conjunct2"]),
    ("All", [thm "spec"]), ("True", []), ("False", []),
isabelle