src/Provers/clasimp.ML
changeset 11462 cf3e7f5ad0e1
parent 11344 57b7ad51971c
child 11496 fa8d12b789e1
     1.1 --- a/src/Provers/clasimp.ML	Mon Aug 06 12:42:43 2001 +0200
     1.2 +++ b/src/Provers/clasimp.ML	Mon Aug 06 12:46:21 2001 +0200
     1.3 @@ -117,25 +117,21 @@
     1.4          the Safe Intr     rule B==>A and
     1.5          the Safe Destruct rule A==>B.
     1.6    Also ~A goes to the Safe Elim rule A ==> ?R
     1.7 -  Failing other cases, A is added as a Safe Intr rule and a warning is issued *)
     1.8 +  Failing other cases, A is added as a Safe Intr rule*)
     1.9  local
    1.10  
    1.11  fun addIff dest elim intro simp ((cs, ss), th) =
    1.12    (          dest (intro (cs, [zero_var_indexes (th RS Data.iffD2)]),
    1.13                                [zero_var_indexes (th RS Data.iffD1)])
    1.14 -   handle THM _ => (warning ("iff add: theorem is not an equivalence\n" 
    1.15 -                  ^ Display.string_of_thm th);
    1.16 -                    elim (cs, [zero_var_indexes (th RS Data.notE )])
    1.17 -   handle THM _ => intro (cs, [th])),
    1.18 +   handle THM _ => (elim (cs, [zero_var_indexes (th RS Data.notE )])
    1.19 +                    handle THM _ => intro (cs, [th])),
    1.20     simp (ss, [th]));
    1.21  
    1.22  fun delIff ((cs, ss), th) =
    1.23 -(                Classical.delrules (cs, [zero_var_indexes (th RS Data.iffD2),
    1.24 -                      Data.cla_make_elim (zero_var_indexes (th RS Data.iffD1))])
    1.25 - handle THM _ => (warning ("iff del: theorem is not an equivalence\n" 
    1.26 -                  ^ Display.string_of_thm th);
    1.27 -                 Classical.delrules (cs, [zero_var_indexes (th RS Data.notE)])
    1.28 - handle THM _ => Classical.delrules (cs, [th])), 
    1.29 +(             Classical.delrules (cs, [zero_var_indexes (th RS Data.iffD2),
    1.30 +                   Data.cla_make_elim (zero_var_indexes (th RS Data.iffD1))])
    1.31 + handle THM _ => (Classical.delrules (cs, [zero_var_indexes (th RS Data.notE)])
    1.32 +                  handle THM _ => Classical.delrules (cs, [th])), 
    1.33   Simplifier.delsimps (ss, [th]));
    1.34  
    1.35  fun store_clasimp (cs, ss) =