author | wenzelm |
Tue, 08 Aug 2000 16:57:44 +0200 | |
changeset 9558 | 8d5221bf765b |
parent 7529 | fa534e4f7e49 |
child 10062 | 3b819da9c71a |
permissions | -rw-r--r-- |
0 | 1 |
|
7355
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5159
diff
changeset
|
2 |
structure FOL = |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5159
diff
changeset
|
3 |
struct |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5159
diff
changeset
|
4 |
val thy = the_context (); |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5159
diff
changeset
|
5 |
val classical = classical; |
4c43090659ca
proper bootstrap of IFOL/FOL theories and packages;
wenzelm
parents:
5159
diff
changeset
|
6 |
end; |
0 | 7 |
|
7529 | 8 |
AddXIs [disjI1, disjI2]; |
9 |
||
0 | 10 |
open FOL; |