isabelle-cookbook: ProgTutorial/Base.thy@db8e302f44c8 (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
210 db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	11	fun inherit_env (context as Context.Proof lthy) =
db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	12	Context.Proof (LocalTheory.map_contexts (ML_Context.inherit_env context) lthy)
db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	13	\| inherit_env context = context;
db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	14
db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	15	fun inherit_env_prf prf = Proof.map_contexts
db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	16	(Context.proof_map (ML_Context.inherit_env (Context.Proof (Proof.context_of prf)))) prf
db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	17
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	18	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	19	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	20	(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	21	(OuterParse.ML_source >> (fn (txt, pos) =>
210 db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	22	Toplevel.generic_theory
db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	23	(ML_Context.exec (fn () => ML_Context.eval true pos txt) #> inherit_env)));
db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	24
db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	25
db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	26	val _ =
db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	27	OuterSyntax.command "ML_prf" "ML text within proof"
db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	28	(OuterKeyword.tag "TutorialML" OuterKeyword.prf_decl)
db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	29	(OuterParse.ML_source >> (fn (txt, pos) =>
db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	30	Toplevel.proof (Proof.map_context (Context.proof_map
db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	31	(ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> inherit_env_prf)))
db8e302f44c8 more work on the simple inductive section Christian Urban <urbanc@in.tum.de> parents: 189 diff changeset	32
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	33	*}
161 83f36a1c62f2 rolled back the changes on the function warning and tracing Christian Urban <urbanc@in.tum.de> parents: 160 diff changeset	34	(*
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	35	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	36	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	37	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	38	*}
161 83f36a1c62f2 rolled back the changes on the function warning and tracing Christian Urban <urbanc@in.tum.de> parents: 160 diff changeset	39	*)
23 1322990e4ee7 New theory for installing antiquotations. berghofe parents: diff changeset	40	end

author	Christian Urban <urbanc@in.tum.de>
	Thu, 26 Mar 2009 19:00:51 +0000
changeset 210	db8e302f44c8
parent 189	069d525f8f1d
child 224	647cab4a72c2
permissions	-rw-r--r--