author | haftmann |
Tue, 29 Jun 2010 11:25:04 +0200 | |
changeset 37613 | 355ec1b521e6 |
parent 31050 | 555b56b66fcf |
child 38405 | 7935b334893e |
permissions | -rw-r--r-- |
20948 | 1 |
|
28419 | 2 |
no_document use_thy "Setup"; |
28420 | 3 |
no_document use_thys ["Efficient_Nat"]; |
28213 | 4 |
|
5 |
use_thy "Introduction"; |
|
6 |
use_thy "Program"; |
|
37613
355ec1b521e6
split off predicate compiler into separate theory
haftmann
parents:
31050
diff
changeset
|
7 |
use_thy "Inductive_Predicate"; |
31050 | 8 |
use_thy "Adaptation"; |
28213 | 9 |
use_thy "Further"; |
28419 | 10 |
use_thy "ML"; |