isabelle-cookbook: CookBook/Base.thy@95e9c4556221 (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"
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	13	(OuterKeyword.tag "CookBookML" OuterKeyword.thy_decl)
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	*}
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	17
80 95e9c4556221 tuned Christian Urban <urbanc@in.tum.de> parents: 64 diff changeset	18
23 1322990e4ee7 New theory for installing antiquotations. berghofe parents: diff changeset	19	end

author	Christian Urban <urbanc@in.tum.de>
	Mon, 26 Jan 2009 12:29:43 +0000
changeset 80	95e9c4556221
parent 64	9a6e5e0c4906
child 106	bdd82350cf22
permissions	-rw-r--r--