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.
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 file | annotate | diff | comparison | revisions
src/HOL/ROOT file | annotate | diff | comparison | revisions 
--- /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
isabelle