equal
deleted
inserted
replaced
1198 Simplifier.method_setup Splitter.split_modifiers |
1198 Simplifier.method_setup Splitter.split_modifiers |
1199 \<close> |
1199 \<close> |
1200 |
1200 |
1201 simproc_setup defined_Ex ("\<exists>x. P x") = \<open>K Quantifier1.rearrange_Ex\<close> |
1201 simproc_setup defined_Ex ("\<exists>x. P x") = \<open>K Quantifier1.rearrange_Ex\<close> |
1202 simproc_setup defined_All ("\<forall>x. P x") = \<open>K Quantifier1.rearrange_All\<close> |
1202 simproc_setup defined_All ("\<forall>x. P x") = \<open>K Quantifier1.rearrange_All\<close> |
|
1203 simproc_setup defined_all("\<And>x. PROP P x") = \<open>K Quantifier1.rearrange_all\<close> |
|
1204 |
|
1205 declare [[simproc del: defined_all]] |
1203 |
1206 |
1204 text \<open>Simproc for proving \<open>(y = x) \<equiv> False\<close> from premise \<open>\<not> (x = y)\<close>:\<close> |
1207 text \<open>Simproc for proving \<open>(y = x) \<equiv> False\<close> from premise \<open>\<not> (x = y)\<close>:\<close> |
1205 |
1208 |
1206 simproc_setup neq ("x = y") = \<open>fn _ => |
1209 simproc_setup neq ("x = y") = \<open>fn _ => |
1207 let |
1210 let |