equal
deleted
inserted
replaced
93 | _ => [th] |
93 | _ => [th] |
94 end; |
94 end; |
95 |
95 |
96 val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, |
96 val ZF_simps = [empty_subsetI, consI1, succI1, ball_simp, if_true, if_false, |
97 beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff, |
97 beta, eta, restrict, fst_conv, snd_conv, split, Pair_iff, |
98 triv_RepFun]; |
98 triv_RepFun, subset_refl]; |
99 |
99 |
100 (*Sigma_cong, Pi_cong NOT included by default since they cause |
100 (*Sigma_cong, Pi_cong NOT included by default since they cause |
101 flex-flex pairs and the "Check your prover" error -- because most |
101 flex-flex pairs and the "Check your prover" error -- because most |
102 Sigma's and Pi's are abbreviated as * or -> *) |
102 Sigma's and Pi's are abbreviated as * or -> *) |
103 val ZF_congs = |
103 val ZF_congs = |