isabelle: src/FOL/FOL.ML@d792570a04b1 (annotated)

0 a5a9c433f639 Initial revision clasohm parents: diff changeset	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 a5a9c433f639 Initial revision clasohm parents: diff changeset	7
11588 d792570a04b1 AddXEs [disjI1, disjI2]; wenzelm parents: 10062 diff changeset	8	AddXIs [equal_intr_rule];
d792570a04b1 AddXEs [disjI1, disjI2]; wenzelm parents: 10062 diff changeset	9	AddXEs [disjI1, disjI2];
7529 fa534e4f7e49 AddXIs [disjI1, disjI2]; wenzelm parents: 7355 diff changeset	10
0 a5a9c433f639 Initial revision clasohm parents: diff changeset	11	open FOL;