| author | wenzelm |
| Thu, 07 Jul 2011 23:55:15 +0200 | |
| changeset 44572 | 91c4d7397f0e |
| parent 40233 | ea46574ca815 |
| child 46321 | dc2236b19a3d |
| permissions | -rw-r--r-- |
| wenzelm@33264 | 1 |
(* Title: HOL/Predicate_Compile.thy |
| wenzelm@33264 | 2 |
Author: Stefan Berghofer, Lukas Bulwahn, Florian Haftmann, TU Muenchen |
| wenzelm@33264 | 3 |
*) |
| bulwahn@33242 | 4 |
|
| bulwahn@33242 | 5 |
header {* A compiler for predicates defined by introduction rules *}
|
| bulwahn@33242 | 6 |
|
| bulwahn@33242 | 7 |
theory Predicate_Compile |
| bulwahn@36015 | 8 |
imports New_Random_Sequence |
| bulwahn@33242 | 9 |
uses |
| bulwahn@33242 | 10 |
"Tools/Predicate_Compile/predicate_compile_aux.ML" |
| bulwahn@36046 | 11 |
"Tools/Predicate_Compile/predicate_compile_compilations.ML" |
| bulwahn@40233 | 12 |
"Tools/Predicate_Compile/core_data.ML" |
| bulwahn@40233 | 13 |
"Tools/Predicate_Compile/mode_inference.ML" |
| bulwahn@40233 | 14 |
"Tools/Predicate_Compile/predicate_compile_proof.ML" |
| bulwahn@33242 | 15 |
"Tools/Predicate_Compile/predicate_compile_core.ML" |
| bulwahn@33242 | 16 |
"Tools/Predicate_Compile/predicate_compile_data.ML" |
| bulwahn@33242 | 17 |
"Tools/Predicate_Compile/predicate_compile_fun.ML" |
| bulwahn@33242 | 18 |
"Tools/Predicate_Compile/predicate_compile_pred.ML" |
| bulwahn@36026 | 19 |
"Tools/Predicate_Compile/predicate_compile_specialisation.ML" |
| bulwahn@33242 | 20 |
"Tools/Predicate_Compile/predicate_compile.ML" |
| bulwahn@33242 | 21 |
begin |
| bulwahn@33242 | 22 |
|
| wenzelm@33264 | 23 |
setup Predicate_Compile.setup |
| bulwahn@33242 | 24 |
|
| bulwahn@34935 | 25 |
end |