isabelle: src/HOL/ROOT.ML@0f6e30b87cf1 (annotated)

29304 5c71a6da989d tuned header and description of boot files; wenzelm parents: 29249 diff changeset	1	(* Classical Higher-order Logic -- batteries included *)
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	2
33113 0f6e30b87cf1 processing of tuples in introduction rules bulwahn parents: 30126 diff changeset	3	Toplevel.debug := true;
29005 ce378dcfddab corrected theory path haftmann parents: 28952 diff changeset	4	use_thy "Complex_Main";
28263 69eaa97e7e96 moved global ML bindings to global place; wenzelm parents: 27421 diff changeset	5
69eaa97e7e96 moved global ML bindings to global place; wenzelm parents: 27421 diff changeset	6	val HOL_proofs = ! Proofterm.proofs;