author | haftmann |
Sat, 28 Apr 2012 09:55:01 +0200 | |
changeset 47819 | d402ac2288b8 |
parent 38510 | ec0408c7328b |
permissions | -rw-r--r-- |
20948 | 1 |
|
28419 | 2 |
no_document use_thy "Setup"; |
28213 | 3 |
|
4 |
use_thy "Introduction"; |
|
38405 | 5 |
use_thy "Foundations"; |
6 |
use_thy "Refinement"; |
|
37613
355ec1b521e6
split off predicate compiler into separate theory
haftmann
parents:
31050
diff
changeset
|
7 |
use_thy "Inductive_Predicate"; |
38510 | 8 |
use_thy "Evaluation"; |
31050 | 9 |
use_thy "Adaptation"; |
28213 | 10 |
use_thy "Further"; |