| author | wenzelm |
| Sun, 10 Jul 2011 00:21:19 +0200 | |
| changeset 43722 | 9b5dadb0c28d |
| parent 41306 | 95449e4b4bf6 |
| permissions | -rw-r--r-- |
|
23914
3e0424305fa4
turned ex/prop.ML, ex/quant.ML into proper theories;
wenzelm
parents:
23156
diff
changeset
|
1 |
use_thys [ |
|
3e0424305fa4
turned ex/prop.ML, ex/quant.ML into proper theories;
wenzelm
parents:
23156
diff
changeset
|
2 |
"First_Order_Logic", |
|
3e0424305fa4
turned ex/prop.ML, ex/quant.ML into proper theories;
wenzelm
parents:
23156
diff
changeset
|
3 |
"Natural_Numbers", |
|
3e0424305fa4
turned ex/prop.ML, ex/quant.ML into proper theories;
wenzelm
parents:
23156
diff
changeset
|
4 |
"Intro", |
|
3e0424305fa4
turned ex/prop.ML, ex/quant.ML into proper theories;
wenzelm
parents:
23156
diff
changeset
|
5 |
"Nat", |
| 29752 | 6 |
"Nat_Class", |
|
23914
3e0424305fa4
turned ex/prop.ML, ex/quant.ML into proper theories;
wenzelm
parents:
23156
diff
changeset
|
7 |
"Foundation", |
|
3e0424305fa4
turned ex/prop.ML, ex/quant.ML into proper theories;
wenzelm
parents:
23156
diff
changeset
|
8 |
"Prolog", |
|
3e0424305fa4
turned ex/prop.ML, ex/quant.ML into proper theories;
wenzelm
parents:
23156
diff
changeset
|
9 |
"Intuitionistic", |
|
3e0424305fa4
turned ex/prop.ML, ex/quant.ML into proper theories;
wenzelm
parents:
23156
diff
changeset
|
10 |
"Propositional_Int", |
|
3e0424305fa4
turned ex/prop.ML, ex/quant.ML into proper theories;
wenzelm
parents:
23156
diff
changeset
|
11 |
"Quantifiers_Int", |
|
3e0424305fa4
turned ex/prop.ML, ex/quant.ML into proper theories;
wenzelm
parents:
23156
diff
changeset
|
12 |
"Classical", |
|
3e0424305fa4
turned ex/prop.ML, ex/quant.ML into proper theories;
wenzelm
parents:
23156
diff
changeset
|
13 |
"Propositional_Cla", |
|
3e0424305fa4
turned ex/prop.ML, ex/quant.ML into proper theories;
wenzelm
parents:
23156
diff
changeset
|
14 |
"Quantifiers_Cla", |
|
3e0424305fa4
turned ex/prop.ML, ex/quant.ML into proper theories;
wenzelm
parents:
23156
diff
changeset
|
15 |
"Miniscope", |
|
40239
c4336e45f199
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref;
wenzelm
parents:
37134
diff
changeset
|
16 |
"If" |
|
23914
3e0424305fa4
turned ex/prop.ML, ex/quant.ML into proper theories;
wenzelm
parents:
23156
diff
changeset
|
17 |
]; |
|
17277
ab45d65bf204
make LocalesTest last, because it sets funny flags;
wenzelm
parents:
16168
diff
changeset
|
18 |
|
| 37134 | 19 |
no_document use_thy "Locale_Test/Locale_Test"; |