isabelle-cookbook: ProgTutorial/Base.thy@d3cd633e8240 (annotated)

23 1322990e4ee7 New theory for installing antiquotations. berghofe parents: diff changeset	1	theory Base
1322990e4ee7 New theory for installing antiquotations. berghofe parents: diff changeset	2	imports Main
1322990e4ee7 New theory for installing antiquotations. berghofe parents: diff changeset	3	uses
57 065f472c09ab Repaired output of marginal comments in ML antiquotation. berghofe parents: 43 diff changeset	4	"chunks.ML"
23 1322990e4ee7 New theory for installing antiquotations. berghofe parents: diff changeset	5	"antiquote_setup.ML"
1322990e4ee7 New theory for installing antiquotations. berghofe parents: diff changeset	6	begin
1322990e4ee7 New theory for installing antiquotations. berghofe parents: diff changeset	7
64 9a6e5e0c4906 deleted old files and added code to give a special tag to the command ML Christian Urban <urbanc@in.tum.de> parents: 57 diff changeset	8	(* to have a special tag for text enclosed in ML *)
9a6e5e0c4906 deleted old files and added code to give a special tag to the command ML Christian Urban <urbanc@in.tum.de> parents: 57 diff changeset	9	ML {*
9a6e5e0c4906 deleted old files and added code to give a special tag to the command ML Christian Urban <urbanc@in.tum.de> parents: 57 diff changeset	10
9a6e5e0c4906 deleted old files and added code to give a special tag to the command ML Christian Urban <urbanc@in.tum.de> parents: 57 diff changeset	11	val _ =
9a6e5e0c4906 deleted old files and added code to give a special tag to the command ML Christian Urban <urbanc@in.tum.de> parents: 57 diff changeset	12	OuterSyntax.command "ML" "eval ML text within theory"
106 bdd82350cf22 renamed in the pdf all instances of cookbook to tutorial (in order to sound more serious) Christian Urban <urbanc@in.tum.de> parents: 80 diff changeset	13	(OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl)
64 9a6e5e0c4906 deleted old files and added code to give a special tag to the command ML Christian Urban <urbanc@in.tum.de> parents: 57 diff changeset	14	(OuterParse.ML_source >> (fn (txt, pos) =>
9a6e5e0c4906 deleted old files and added code to give a special tag to the command ML Christian Urban <urbanc@in.tum.de> parents: 57 diff changeset	15	Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt))));
9a6e5e0c4906 deleted old files and added code to give a special tag to the command ML Christian Urban <urbanc@in.tum.de> parents: 57 diff changeset	16	*}
161 83f36a1c62f2 rolled back the changes on the function warning and tracing Christian Urban <urbanc@in.tum.de> parents: 160 diff changeset	17	(*
160 cc9359bfacf4 redefined the functions warning and tracing in order to properly match more antiquotations Christian Urban <urbanc@in.tum.de> parents: 106 diff changeset	18	ML {*
cc9359bfacf4 redefined the functions warning and tracing in order to properly match more antiquotations Christian Urban <urbanc@in.tum.de> parents: 106 diff changeset	19	fun warning str = str
cc9359bfacf4 redefined the functions warning and tracing in order to properly match more antiquotations Christian Urban <urbanc@in.tum.de> parents: 106 diff changeset	20	fun tracing str = str
cc9359bfacf4 redefined the functions warning and tracing in order to properly match more antiquotations Christian Urban <urbanc@in.tum.de> parents: 106 diff changeset	21	*}
161 83f36a1c62f2 rolled back the changes on the function warning and tracing Christian Urban <urbanc@in.tum.de> parents: 160 diff changeset	22	*)
23 1322990e4ee7 New theory for installing antiquotations. berghofe parents: diff changeset	23	end

author	Christian Urban <urbanc@in.tum.de>
	Tue, 24 Mar 2009 12:09:38 +0100
changeset 207	d3cd633e8240
parent 189	069d525f8f1d
child 210	db8e302f44c8
permissions	-rw-r--r--