src/HOL/Main.thy
changeset 18510 0a6c24f549c3
parent 18315 e52f867ab851
child 19607 07eeb832f28d
     1.1 --- a/src/HOL/Main.thy	Fri Dec 23 17:36:00 2005 +0100
     1.2 +++ b/src/HOL/Main.thy	Fri Dec 23 17:37:54 2005 +0100
     1.3 @@ -18,11 +18,6 @@
     1.4    claset rules into the clause cache; cf.\ theory @{text
     1.5    Reconstruction}. *}
     1.6  
     1.7 -declare subset_refl [intro] 
     1.8 -  text {*Ensures that this important theorem is not superseded by the
     1.9 -         simplifier's "== True" version.*}
    1.10 -setup ResAxioms.clause_setup
    1.11 -declare subset_refl [rule del]
    1.12 -  text {*Removed again because it harms blast's performance.*}
    1.13 +setup ResAxioms.setup
    1.14  
    1.15  end