src/FOL/simpdata.ML
changeset 20223 89d2758ecddf
parent 18708 4b3dadb4fe33
child 21539 c5cf9243ad62
     1.1 --- a/src/FOL/simpdata.ML	Thu Jul 27 13:42:59 2006 +0200
     1.2 +++ b/src/FOL/simpdata.ML	Thu Jul 27 13:43:00 2006 +0200
     1.3 @@ -6,14 +6,9 @@
     1.4  Simplification data for FOL.
     1.5  *)
     1.6  
     1.7 -
     1.8 -(* Elimination of True from asumptions: *)
     1.9 +val ex1_functional = thm "ex1_functional";
    1.10 +val True_implies_equals = thm "True_implies_equals";
    1.11  
    1.12 -bind_thm ("True_implies_equals", prove_goal IFOL.thy
    1.13 - "(True ==> PROP P) == PROP P"
    1.14 -(K [rtac equal_intr_rule 1, atac 2,
    1.15 -          METAHYPS (fn prems => resolve_tac prems 1) 1,
    1.16 -          rtac TrueI 1]));
    1.17  
    1.18  
    1.19  (*** Rewrite rules ***)