author | haftmann |
Tue, 03 Mar 2020 19:26:24 +0000 | |
changeset 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 |