src/FOL/simpdata.ML
changeset 12725 7ede865e1fe5
parent 12720 f8a134b9a57f
child 12765 fb3f9887d0b7
equal deleted inserted replaced
12724:beedc794bd67 12725:7ede865e1fe5
   119                    | None => [th])
   119                    | None => [th])
   120               | _ => [th])
   120               | _ => [th])
   121          | _ => [th])
   121          | _ => [th])
   122   in atoms end;
   122   in atoms end;
   123 
   123 
   124 fun mksimps pairs = (map mk_eq o mk_atomize pairs o forall_elim_vars_safe);
   124 fun mksimps pairs = (map mk_eq o mk_atomize pairs o gen_all);
   125 
   125 
   126 (*** Classical laws ***)
   126 (*** Classical laws ***)
   127 
   127 
   128 fun prove_fun s =
   128 fun prove_fun s =
   129  (writeln s;
   129  (writeln s;