discontinued obsolete ML antiquotation @{claset};
authorwenzelm
Wed Apr 10 17:17:16 2013 +0200 (2013-04-10)
changeset 516873d8720271ebf
parent 51686 532e0ac5a66d
child 51688 27ecd33d3366
discontinued obsolete ML antiquotation @{claset};
src/FOL/FOL.thy
src/HOL/HOL.thy
     1.1 --- a/src/FOL/FOL.thy	Wed Apr 10 17:02:47 2013 +0200
     1.2 +++ b/src/FOL/FOL.thy	Wed Apr 10 17:17:16 2013 +0200
     1.3 @@ -181,24 +181,19 @@
     1.4  open Basic_Classical;
     1.5  *}
     1.6  
     1.7 -setup {*
     1.8 -  ML_Antiquote.value @{binding claset}
     1.9 -    (Scan.succeed "Cla.claset_of ML_context")
    1.10 -*}
    1.11 -
    1.12  setup Cla.setup
    1.13  
    1.14  (*Propositional rules*)
    1.15  lemmas [intro!] = refl TrueI conjI disjCI impI notI iffI
    1.16    and [elim!] = conjE disjE impCE FalseE iffCE
    1.17 -ML {* val prop_cs = @{claset} *}
    1.18 +ML {* val prop_cs = claset_of @{context} *}
    1.19  
    1.20  (*Quantifier rules*)
    1.21  lemmas [intro!] = allI ex_ex1I
    1.22    and [intro] = exI
    1.23    and [elim!] = exE alt_ex1E
    1.24    and [elim] = allE
    1.25 -ML {* val FOL_cs = @{claset} *}
    1.26 +ML {* val FOL_cs = claset_of @{context} *}
    1.27  
    1.28  ML {*
    1.29    structure Blast = Blast
     2.1 --- a/src/HOL/HOL.thy	Wed Apr 10 17:02:47 2013 +0200
     2.2 +++ b/src/HOL/HOL.thy	Wed Apr 10 17:17:16 2013 +0200
     2.3 @@ -843,11 +843,6 @@
     2.4  open Basic_Classical;
     2.5  *}
     2.6  
     2.7 -setup {*
     2.8 -  ML_Antiquote.value @{binding claset}
     2.9 -    (Scan.succeed "Classical.claset_of ML_context")
    2.10 -*}
    2.11 -
    2.12  setup Classical.setup
    2.13  
    2.14  setup {*
    2.15 @@ -888,7 +883,7 @@
    2.16  declare exE [elim!]
    2.17    allE [elim]
    2.18  
    2.19 -ML {* val HOL_cs = @{claset} *}
    2.20 +ML {* val HOL_cs = claset_of @{context} *}
    2.21  
    2.22  lemma contrapos_np: "~ Q ==> (~ P ==> Q) ==> P"
    2.23    apply (erule swap)