equal
deleted
inserted
replaced
88 |
88 |
89 |
89 |
90 lemmas [simp del] = ex_simps all_simps split_paired_Ex |
90 lemmas [simp del] = ex_simps all_simps split_paired_Ex |
91 declare Let_def [simp] |
91 declare Let_def [simp] |
92 |
92 |
93 ML_setup {* change_claset (fn cs => cs delSWrapper "split_all_tac") *} |
93 declaration {* fn _ => Classical.map_cs (fn cs => cs delSWrapper "split_all_tac") *} |
94 |
94 |
95 |
95 |
96 subsection {* ex2seqC *} |
96 subsection {* ex2seqC *} |
97 |
97 |
98 lemma ex2seqC_unfold: "ex2seqC = (LAM ex. (%s. case ex of |
98 lemma ex2seqC_unfold: "ex2seqC = (LAM ex. (%s. case ex of |