equal
deleted
inserted
replaced
78 val exE = @{thm exE} |
78 val exE = @{thm exE} |
79 val iff_allI = @{thm iff_allI} |
79 val iff_allI = @{thm iff_allI} |
80 val iff_exI = @{thm iff_exI} |
80 val iff_exI = @{thm iff_exI} |
81 val all_comm = @{thm all_comm} |
81 val all_comm = @{thm all_comm} |
82 val ex_comm = @{thm ex_comm} |
82 val ex_comm = @{thm ex_comm} |
|
83 val atomize = |
|
84 let val rules = @{thms atomize_all atomize_imp atomize_eq atomize_iff atomize_conj} |
|
85 in fn ctxt => Raw_Simplifier.rewrite ctxt true rules end |
83 ); |
86 ); |
84 |
87 |
85 |
88 |
86 (*** Case splitting ***) |
89 (*** Case splitting ***) |
87 |
90 |