author | wenzelm |
Thu, 07 Sep 2000 20:47:34 +0200 | |
changeset 9885 | 34494703d283 |
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; |