author | wenzelm |
Fri, 31 Aug 2001 22:45:08 +0200 | |
changeset 11541 | 09dc5e8ac99c |
parent 10062 | 3b819da9c71a |
child 11588 | d792570a04b1 |
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 |
|
10062 | 8 |
AddXIs [equal_intr_rule, disjI1, disjI2]; |
7529 | 9 |
|
0 | 10 |
open FOL; |