isabelle: src/Pure/ML_Bootstrap.thy@51ac6bc389e8 (annotated)

62887 6b2c60ebd915 clarified ML bootstrap environment; wenzelm parents: 62883 diff changeset	1	(* Title: Pure/ML_Bootstrap.thy
62868 61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	2	Author: Makarius
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	3
62887 6b2c60ebd915 clarified ML bootstrap environment; wenzelm parents: 62883 diff changeset	4	ML bootstrap environment -- with access to low-level structures!
62868 61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	5	*)
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	6
62887 6b2c60ebd915 clarified ML bootstrap environment; wenzelm parents: 62883 diff changeset	7	theory ML_Bootstrap
62880 76e7d9169b54 clarified files; wenzelm parents: 62873 diff changeset	8	imports Pure
62868 61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	9	begin
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	10
62873 2f9c8a18f832 support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML; wenzelm parents: 62871 diff changeset	11	setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>
62930 51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: 62902 diff changeset	12
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: 62902 diff changeset	13	SML_import \<open>
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: 62902 diff changeset	14	structure Output_Primitives = Output_Primitives_Virtual;
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: 62902 diff changeset	15	structure Thread_Data = Thread_Data_Virtual;
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: 62902 diff changeset	16	\<close>
51ac6bc389e8 shared output primitives of physical/virtual Pure; wenzelm parents: 62902 diff changeset	17
62902 3c0f53eae166 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; wenzelm parents: 62893 diff changeset	18	setup \<open>Config.put_global ML_Env.SML_environment true\<close>
62868 61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	19
61a691db1c4d support for ML project ROOT file, with imitation of ML "use" commands; wenzelm parents: diff changeset	20	end

author	wenzelm
	Sat, 09 Apr 2016 16:16:05 +0200
changeset 62930	51ac6bc389e8
parent 62902	3c0f53eae166
child 62944	3ee643c5ed00
permissions	-rw-r--r--