| author | wenzelm |
| Mon, 13 Apr 2020 22:08:14 +0200 | |
| changeset 71751 | abf3e80bd815 |
| parent 71518 | bae868febc53 |
| child 71886 | 4f4695757980 |
| permissions | -rw-r--r-- |
|
71518
bae868febc53
library theory for extractions of equations x = t into premises
haftmann
parents:
diff
changeset
|
1 |
(* Author: Florian Haftmann, TU München *) |
|
bae868febc53
library theory for extractions of equations x = t into premises
haftmann
parents:
diff
changeset
|
2 |
|
|
bae868febc53
library theory for extractions of equations x = t into premises
haftmann
parents:
diff
changeset
|
3 |
theory Quantified_Premise_Simproc |
|
bae868febc53
library theory for extractions of equations x = t into premises
haftmann
parents:
diff
changeset
|
4 |
imports Main |
|
bae868febc53
library theory for extractions of equations x = t into premises
haftmann
parents:
diff
changeset
|
5 |
begin |
|
bae868febc53
library theory for extractions of equations x = t into premises
haftmann
parents:
diff
changeset
|
6 |
|
|
bae868febc53
library theory for extractions of equations x = t into premises
haftmann
parents:
diff
changeset
|
7 |
simproc_setup defined_forall ("\<And>x. PROP P x") = \<open>K Quantifier1.rearrange_All\<close>
|
|
bae868febc53
library theory for extractions of equations x = t into premises
haftmann
parents:
diff
changeset
|
8 |
|
|
bae868febc53
library theory for extractions of equations x = t into premises
haftmann
parents:
diff
changeset
|
9 |
end |