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

1264 3eb91524b938 added local simpsets; removed IOA from 'make test' clasohm parents: 1165 diff changeset	1	(* Title: HOL/ROOT.ML
23166 45f3c90b2d27 proper loading of ML files (in HOL.thy); wenzelm parents: 22997 diff changeset	2
27368 9f90ac19e32b established Plain theory and image haftmann parents: 25964 diff changeset	3	Classical Higher-order Logic -- batteries included.
923 ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	4	*)
ff1574a81019 new version of HOL with curried function application clasohm parents: diff changeset	5
29233 ce6d35a0bed6 Ported HOL and HOL-Library to new locales. ballarin parents: 29005 diff changeset	6	set new_locales;
29005 ce378dcfddab corrected theory path haftmann parents: 28952 diff changeset	7	use_thy "Complex_Main";
28263 69eaa97e7e96 moved global ML bindings to global place; wenzelm parents: 27421 diff changeset	8
69eaa97e7e96 moved global ML bindings to global place; wenzelm parents: 27421 diff changeset	9	val HOL_proofs = ! Proofterm.proofs;
69eaa97e7e96 moved global ML bindings to global place; wenzelm parents: 27421 diff changeset	10