src/HOL/simpdata.ML
changeset 6968 7f2977e96a5c
parent 6915 4ab8e31a8421
child 7031 972b5f62f476
equal deleted inserted replaced
6967:a3c163ed1e04 6968:7f2977e96a5c
    29                     then cla addSIs [zero_var_indexes (th RS iffD2)]  
    29                     then cla addSIs [zero_var_indexes (th RS iffD2)]  
    30                               addSDs [zero_var_indexes (th RS iffD1)]
    30                               addSDs [zero_var_indexes (th RS iffD1)]
    31                     else  cla addSIs [th]
    31                     else  cla addSIs [th]
    32               | _ => cla addSIs [th],
    32               | _ => cla addSIs [th],
    33        simp addsimps [th])
    33        simp addsimps [th])
    34       handle _ => error ("AddIffs: theorem must be unconditional\n" ^ 
    34       handle TERM _ => error ("AddIffs: theorem must be unconditional\n" ^ 
    35                          string_of_thm th);
    35                          string_of_thm th);
    36 
    36 
    37   fun delIff ((cla, simp), th) = 
    37   fun delIff ((cla, simp), th) = 
    38       (case HOLogic.dest_Trueprop (#prop (rep_thm th)) of
    38       (case HOLogic.dest_Trueprop (#prop (rep_thm th)) of
    39                 (Const ("Not", _) $ A) =>
    39                 (Const ("Not", _) $ A) =>
    43                     then cla delrules [zero_var_indexes (th RS iffD2),
    43                     then cla delrules [zero_var_indexes (th RS iffD2),
    44                                        make_elim (zero_var_indexes (th RS iffD1))]
    44                                        make_elim (zero_var_indexes (th RS iffD1))]
    45                     else cla delrules [th]
    45                     else cla delrules [th]
    46               | _ => cla delrules [th],
    46               | _ => cla delrules [th],
    47        simp delsimps [th])
    47        simp delsimps [th])
    48       handle _ => (warning("DelIffs: ignoring conditional theorem\n" ^ 
    48       handle TERM _ => (warning("DelIffs: ignoring conditional theorem\n" ^ 
    49                           string_of_thm th); (cla, simp));
    49                           string_of_thm th); (cla, simp));
    50 
    50 
    51   fun store_clasimp (cla, simp) = (claset_ref () := cla; simpset_ref () := simp)
    51   fun store_clasimp (cla, simp) = (claset_ref () := cla; simpset_ref () := simp)
    52 in
    52 in
    53 val op addIffs = foldl addIff;
    53 val op addIffs = foldl addIff;