Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
activate simproc for FOL
authorhaftmann
Thu, 04 Jun 2020 15:30:22 +0000
changeset 71920 b0da0537f307
parent 71919 2e7df6774373
child 71921 a238074c5a9d
activate simproc for FOL
src/FOL/FOL.thy file | annotate | diff | comparison | revisions 
--- a/src/FOL/FOL.thy	Thu Jun 04 15:30:22 2020 +0000
+++ b/src/FOL/FOL.thy	Thu Jun 04 15:30:22 2020 +0000
@@ -337,8 +337,9 @@
 
 ML_file \<open>simpdata.ML\<close>
 
-simproc_setup defined_Ex (\<open>\<exists>x. P(x)\<close>) = \<open>fn _ => Quantifier1.rearrange_Ex\<close>
-simproc_setup defined_All (\<open>\<forall>x. P(x)\<close>) = \<open>fn _ => Quantifier1.rearrange_All\<close>
+simproc_setup defined_Ex (\<open>\<exists>x. P(x)\<close>) = \<open>K Quantifier1.rearrange_Ex\<close>
+simproc_setup defined_All (\<open>\<forall>x. P(x)\<close>) = \<open>K Quantifier1.rearrange_All\<close>
+simproc_setup defined_all("\<And>x. PROP P(x)") = \<open>K Quantifier1.rearrange_all\<close>
 
 ML \<open>
 (*intuitionistic simprules only*)
isabelle