isabelle: src/HOL/ROOT.ML@261abc2e3155 (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
33615 261abc2e3155 uniform use of simultabeous use_thys; wenzelm parents: 30126 diff changeset	3	use_thys ["Complex_Main"];
28263 69eaa97e7e96 moved global ML bindings to global place; wenzelm parents: 27421 diff changeset	4
69eaa97e7e96 moved global ML bindings to global place; wenzelm parents: 27421 diff changeset	5	val HOL_proofs = ! Proofterm.proofs;