77 Const(a,_) => |
77 Const(a,_) => |
78 (case assoc(pairs,a) of |
78 (case assoc(pairs,a) of |
79 Some rls => flat (map atomize ([th] RL rls)) |
79 Some rls => flat (map atomize ([th] RL rls)) |
80 | None => [th]) |
80 | None => [th]) |
81 | _ => [th] |
81 | _ => [th] |
82 in case concl_of th of (*The operator below is Trueprop*) |
82 in case concl_of th of |
83 _ $ (Const("op :",_) $ a $ b) => tryrules atomize_mem_pairs b |
83 Const("Trueprop",_) $ P => |
84 | _ $ (Const("True",_)) => [] (*True is DELETED*) |
84 (case P of |
85 | _ $ (Const("False",_)) => [] (*should False do something??*) |
85 Const("op :",_) $ a $ b => tryrules atomize_mem_pairs b |
86 | _ $ A => tryrules atomize_pairs A |
86 | Const("True",_) => [] |
|
87 | Const("False",_) => [] |
|
88 | A => tryrules atomize_pairs A) |
|
89 | _ => [th] |
87 end; |
90 end; |
88 |
91 |
89 val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, |
92 val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, |
90 beta, eta, restrict, fst_conv, snd_conv, split]; |
93 beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff]; |
91 |
94 |
92 (*Sigma_cong, Pi_cong NOT included by default since they cause |
95 (*Sigma_cong, Pi_cong NOT included by default since they cause |
93 flex-flex pairs and the "Check your prover" error -- because most |
96 flex-flex pairs and the "Check your prover" error -- because most |
94 Sigma's and Pi's are abbreviated as * or -> *) |
97 Sigma's and Pi's are abbreviated as * or -> *) |
95 val ZF_congs = |
98 val ZF_congs = |