src/HOL/simpdata.ML
changeset 22128 cdd92316dd31
parent 21674 8a6bf9d7c751
child 22147 f4ed4d940d44
     1.1 --- a/src/HOL/simpdata.ML	Sat Jan 20 14:09:10 2007 +0100
     1.2 +++ b/src/HOL/simpdata.ML	Sat Jan 20 14:09:11 2007 +0100
     1.3 @@ -177,9 +177,12 @@
     1.4  structure Clasimp = ClasimpFun
     1.5   (structure Simplifier = Simplifier and Splitter = Splitter
     1.6    and Classical  = Classical and Blast = Blast
     1.7 -  val iffD1 = thm "iffD1" val iffD2 = thm "iffD2" val notE = thm "notE")
     1.8 +  val iffD1 = thm "iffD1" val iffD2 = thm "iffD2" val notE = thm "notE");
     1.9  open Clasimp;
    1.10  
    1.11 +val _ = ML_Context.value_antiq "clasimpset"
    1.12 +  (Scan.succeed ("clasimpset", "Clasimp.local_clasimpset_of (ML_Context.the_local_context ())"));
    1.13 +
    1.14  val mksimps_pairs =
    1.15    [("op -->", [thm "mp"]), ("op &", [thm "conjunct1", thm "conjunct2"]),
    1.16     ("All", [thm "spec"]), ("True", []), ("False", []),