equal
deleted
inserted
replaced
72 | _ $ (Const("All",_) $ _) => atomize(th RS spec) |
72 | _ $ (Const("All",_) $ _) => atomize(th RS spec) |
73 | _ $ (Const("True",_)) => [] |
73 | _ $ (Const("True",_)) => [] |
74 | _ $ (Const("False",_)) => [] |
74 | _ $ (Const("False",_)) => [] |
75 | _ => [th]; |
75 | _ => [th]; |
76 |
76 |
77 fun mk_rew_rules th = map mk_meta_eq (atomize th); |
77 fun gen_all th = forall_elim_vars (#maxidx(rep_thm th)+1) th; |
|
78 |
|
79 fun mk_rew_rules th = map mk_meta_eq (atomize(gen_all th)); |
78 |
80 |
79 structure Induction = InductionFun(struct val spec=IFOL.spec end); |
81 structure Induction = InductionFun(struct val spec=IFOL.spec end); |
80 |
82 |
81 val IFOL_rews = |
83 val IFOL_rews = |
82 [refl_iff_T] @ conj_rews @ disj_rews @ not_rews @ |
84 [refl_iff_T] @ conj_rews @ disj_rews @ not_rews @ |