equal
deleted
inserted
replaced
78 val iff_exI = @{thm iff_exI} |
78 val iff_exI = @{thm iff_exI} |
79 val all_comm = @{thm all_comm} |
79 val all_comm = @{thm all_comm} |
80 val ex_comm = @{thm ex_comm} |
80 val ex_comm = @{thm ex_comm} |
81 end); |
81 end); |
82 |
82 |
83 val defEX_regroup = |
|
84 Simplifier.simproc_global @{theory} |
|
85 "defined EX" ["EX x. P(x)"] Quantifier1.rearrange_ex; |
|
86 |
|
87 val defALL_regroup = |
|
88 Simplifier.simproc_global @{theory} |
|
89 "defined ALL" ["ALL x. P(x)"] Quantifier1.rearrange_all; |
|
90 |
|
91 |
83 |
92 (*** Case splitting ***) |
84 (*** Case splitting ***) |
93 |
85 |
94 structure Splitter = Splitter |
86 structure Splitter = Splitter |
95 ( |
87 ( |