isabelle: src/HOL/ROOT.ML@a2baf1b221be (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
29447 a5d0c3cf305f load main entry points sequentially, for reduced memory demands; wenzelm parents: 29304 diff changeset	3	use_thy "Main";
29638 1f8f3d26a2cf added share_common_data -- reduces heap space, but takes long; wenzelm parents: 29447 diff changeset	4	share_common_data ();
29005 ce378dcfddab corrected theory path haftmann parents: 28952 diff changeset	5	use_thy "Complex_Main";
28263 69eaa97e7e96 moved global ML bindings to global place; wenzelm parents: 27421 diff changeset	6
69eaa97e7e96 moved global ML bindings to global place; wenzelm parents: 27421 diff changeset	7	val HOL_proofs = ! Proofterm.proofs;