library theory for extractions of equations x = t into premises
authorhaftmann
Tue, 03 Mar 2020 19:26:24 +0000
changeset 71518 bae868febc53
parent 71517 7807d828a061
child 71519 8a96a11e0cf5
library theory for extractions of equations x = t into premises
src/HOL/Library/Quantified_Premise_Simproc.thy
src/HOL/ROOT
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Quantified_Premise_Simproc.thy	Tue Mar 03 19:26:24 2020 +0000
@@ -0,0 +1,9 @@
+(* Author: Florian Haftmann, TU M√ľnchen *)
+
+theory Quantified_Premise_Simproc
+  imports Main
+begin
+
+simproc_setup defined_forall ("\<And>x. PROP P x") = \<open>K Quantifier1.rearrange_All\<close>
+
+end
--- a/src/HOL/ROOT	Tue Mar 03 19:26:23 2020 +0000
+++ b/src/HOL/ROOT	Tue Mar 03 19:26:24 2020 +0000
@@ -52,6 +52,7 @@
     OptionalSugar
     (*prototypic tools*)
     Predicate_Compile_Quickcheck
+    Quantified_Premise_Simproc
     (*legacy tools*)
     Old_Datatype
     Old_Recdef