--- a/CookBook/Package/Ind_Code.thy Tue Mar 10 13:20:46 2009 +0000
+++ b/CookBook/Package/Ind_Code.thy Wed Mar 11 01:43:28 2009 +0000
@@ -94,13 +94,14 @@
The actual definitions are made in Line 7.
*}
-subsection {* Introduction Rules *}
+
+subsection {* Induction Principles *}
ML{*fun inst_spec ct =
Drule.instantiate' [SOME (ctyp_of_term ct)] [NONE, SOME ct] @{thm spec}*}
text {*
- Instantiates the @{text "x"} in @{thm spec[no_vars]} with a @{ML_type cterm}.
+ Instantiates the @{text "?x"} in @{thm spec} with a @{ML_type cterm}.
*}
text {*
@@ -110,44 +111,72 @@
lemma "\<forall>x\<^isub>1 x\<^isub>2 x\<^isub>3. P (x\<^isub>1::nat) (x\<^isub>2::nat) (x\<^isub>3::nat) \<Longrightarrow> True"
apply (tactic {* EVERY' (map (dtac o inst_spec)
[@{cterm "y\<^isub>1::nat"},@{cterm "y\<^isub>2::nat"},@{cterm "y\<^isub>3::nat"}]) 1*})
+txt {* \begin{minipage}{\textwidth}
+ @{subgoals}
+ \end{minipage}*}
(*<*)oops(*>*)
+
+lemma
+ assumes "even n"
+ shows "P 0 \<Longrightarrow>
+ (\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
+apply(atomize (full))
+apply(cut_tac prems)
+apply(unfold even_def)
+apply(drule spec[where x=P])
+apply(drule spec[where x=Q])
+apply(assumption)
+done
+
text {*
The tactic for proving the induction rules:
*}
ML{*fun induction_tac defs prems insts =
- EVERY1 [ObjectLogic.full_atomize_tac,
+ EVERY1 [K (print_tac "start"),
+ ObjectLogic.full_atomize_tac,
cut_facts_tac prems,
K (rewrite_goals_tac defs),
EVERY' (map (dtac o inst_spec) insts),
assume_tac]*}
lemma
- assumes asm: "even n"
+ assumes "even n"
shows "P 0 \<Longrightarrow>
(\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
-apply(tactic {* induction_tac [@{thm even_def}, @{thm odd_def}] [@{thm asm}]
- [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}] *})
+apply(tactic {*
+ let
+ val defs = [@{thm even_def}, @{thm odd_def}]
+ val insts = [@{cterm "P::nat\<Rightarrow>bool"}, @{cterm "Q::nat\<Rightarrow>bool"}]
+ in
+ induction_tac defs @{thms prems} insts
+ end *})
done
-ML %linenosgray{*fun inductions rules defs preds Tss lthy1 =
+text {*
+ While the generic proof is relatively simple, it is a bit harder to
+ set up the goals for the induction principles.
+*}
+
+
+ML %linenosgray{*fun inductions rules defs preds tyss lthy1 =
let
val Ps = replicate (length preds) "P"
val (newprednames, lthy2) = Variable.variant_fixes Ps lthy1
val thy = ProofContext.theory_of lthy2
- val Tss' = map (fn Ts => Ts ---> HOLogic.boolT) Tss
- val newpreds = map Free (newprednames ~~ Tss')
+ val tyss' = map (fn tys => tys ---> HOLogic.boolT) tyss
+ val newpreds = map Free (newprednames ~~ tyss')
val cnewpreds = map (cterm_of thy) newpreds
val rules' = map (subst_free (preds ~~ newpreds)) rules
- fun prove_induction ((pred, newpred), Ts) =
+ fun prove_induction ((pred, newpred), tys) =
let
- val zs = replicate (length Ts) "z"
+ val zs = replicate (length tys) "z"
val (newargnames, lthy3) = Variable.variant_fixes zs lthy2;
- val newargs = map Free (newargnames ~~ Ts)
+ val newargs = map Free (newargnames ~~ tys)
val prem = HOLogic.mk_Trueprop (list_comb (pred, newargs))
val goal = Logic.list_implies
@@ -158,26 +187,137 @@
|> singleton (ProofContext.export lthy3 lthy1)
end
in
- map prove_induction (preds ~~ newpreds ~~ Tss)
+ map prove_induction (preds ~~ newpreds ~~ tyss)
+end*}
+
+(*
+ML {*
+ let
+ val rules = [@{term "even 0"},
+ @{term "\<And>n::nat. odd n \<Longrightarrow> even (Suc n)"},
+ @{term "\<And>n::nat. even n \<Longrightarrow> odd (Suc n)"}]
+ val defs = [@{thm even_def}, @{thm odd_def}]
+ val preds = [@{term "even::nat\<Rightarrow>bool"}, @{term "odd::nat\<Rightarrow>bool"}]
+ val tyss = [[@{typ "nat"}],[@{typ "nat"}]]
+ in
+ inductions rules defs preds tyss @{context}
+ end
+*}
+*)
+
+subsection {* Introduction Rules *}
+
+ML{*val all_elims = fold (fn ct => fn th => th RS inst_spec ct)
+val imp_elims = fold (fn th => fn th' => [th', th] MRS @{thm mp})*}
+
+ML{*fun subproof2 prem params2 prems2 =
+ SUBPROOF (fn {prems, ...} =>
+ let
+ val prem' = prems MRS prem;
+ val prem'' =
+ case prop_of prem' of
+ _ $ (Const (@{const_name All}, _) $ _) =>
+ prem' |> all_elims params2
+ |> imp_elims prems2
+ | _ => prem';
+ in
+ rtac prem'' 1
+ end)*}
+
+ML{*fun subproof1 rules preds i =
+ SUBPROOF (fn {params, prems, context = ctxt', ...} =>
+ let
+ val (prems1, prems2) = chop (length prems - length rules) prems;
+ val (params1, params2) = chop (length params - length preds) params;
+ in
+ rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
+ THEN
+ EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1)
+ end)*}
+
+ML{*
+fun introductions_tac defs rules preds i ctxt =
+ EVERY1 [ObjectLogic.rulify_tac,
+ K (rewrite_goals_tac defs),
+ REPEAT o (resolve_tac [@{thm allI},@{thm impI}]),
+ subproof1 rules preds i ctxt]*}
+
+ML{*fun introductions rules preds defs lthy =
+let
+ fun prove_intro (i, goal) =
+ Goal.prove lthy [] [] goal
+ (fn {context, ...} => introductions_tac defs rules preds i context)
+in
+ map_index prove_intro rules
end*}
-ML {* Goal.prove *}
-ML {* singleton *}
-ML {* ProofContext.export *}
+ML %linenosgray{*fun add_inductive_i pred_specs rule_specs lthy =
+let
+ val syns = map snd pred_specs
+ val pred_specs' = map fst pred_specs
+ val prednames = map fst pred_specs'
+ val preds = map (fn (p, ty) => Free (Binding.name_of p, ty)) pred_specs'
-text {*
+ val tyss = map (binder_types o fastype_of) preds
+ val (attrs, rules) = split_list rule_specs
+
+ val (defs, lthy') = definitions rules preds prednames syns tyss lthy
+ val ind_rules = inductions rules defs preds tyss lthy'
+ val intro_rules = introductions rules preds defs lthy'
-*}
-
-text {*
- @{ML_chunk [display,gray] subproof1}
-
- @{ML_chunk [display,gray] subproof2}
-
- @{ML_chunk [display,gray] intro_rules}
+ val mut_name = space_implode "_" (map Binding.name_of prednames)
+ val case_names = map (Binding.name_of o fst) attrs
+in
+ lthy'
+ |> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) =>
+ ((Binding.qualify false mut_name a, atts), [([th], [])])) (rule_specs ~~ intro_rules))
+ |-> (fn intross => LocalTheory.note Thm.theoremK
+ ((Binding.qualify false mut_name (Binding.name "intros"), []), maps snd intross))
+ |>> snd
+ ||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) =>
+ ((Binding.qualify false (Binding.name_of R) (Binding.name "induct"),
+ [Attrib.internal (K (RuleCases.case_names case_names)),
+ Attrib.internal (K (RuleCases.consumes 1)),
+ Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])]))
+ (pred_specs ~~ ind_rules)) #>> maps snd)
+ |> snd
+end*}
-*}
+ML{*fun read_specification' vars specs lthy =
+let
+ val specs' = map (fn (a, s) => [(a, [s])]) specs
+ val ((varst, specst), _) =
+ Specification.read_specification vars specs' lthy
+ val specst' = map (apsnd the_single) specst
+in
+ (varst, specst')
+end*}
+
+ML{*fun add_inductive pred_specs rule_specs lthy =
+let
+ val (pred_specs', rule_specs') =
+ read_specification' pred_specs rule_specs lthy
+in
+ add_inductive_i pred_specs' rule_specs' lthy
+end*}
+
+ML{*val spec_parser =
+ OuterParse.opt_target --
+ OuterParse.fixes --
+ Scan.optional
+ (OuterParse.$$$ "where" |--
+ OuterParse.!!!
+ (OuterParse.enum1 "|"
+ (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []*}
+
+ML{*val specification =
+ spec_parser >>
+ (fn ((loc, pred_specs), rule_specs) =>
+ Toplevel.local_theory loc (add_inductive pred_specs rule_specs))*}
+
+ML{*val _ = OuterSyntax.command "simple_inductive" "define inductive predicates"
+ OuterKeyword.thy_decl specification*}
text {*
Things to include at the end:
@@ -191,5 +331,11 @@
*}
+simple_inductive
+ Even and Odd
+where
+ Even0: "Even 0"
+| EvenS: "Odd n \<Longrightarrow> Even (Suc n)"
+| OddS: "Even n \<Longrightarrow> Odd (Suc n)"
end
--- a/CookBook/Package/Ind_Prelims.thy Tue Mar 10 13:20:46 2009 +0000
+++ b/CookBook/Package/Ind_Prelims.thy Wed Mar 11 01:43:28 2009 +0000
@@ -75,10 +75,10 @@
*}
lemma %linenos trcl_induct:
- assumes asm: "trcl R x y"
+ assumes "trcl R x y"
shows "(\<And>x. P x x) \<Longrightarrow> (\<And>x y z. R x y \<Longrightarrow> P y z \<Longrightarrow> P x z) \<Longrightarrow> P x y"
apply(atomize (full))
-apply(cut_tac asm)
+apply(cut_tac prems)
apply(unfold trcl_def)
apply(drule spec[where x=P])
apply(assumption)
@@ -212,11 +212,11 @@
*}
simple_inductive
- even\<iota> and odd\<iota>
+ even and odd
where
- even0: "even\<iota> 0"
-| evenS: "odd\<iota> n \<Longrightarrow> even\<iota> (Suc n)"
-| oddS: "even\<iota> n \<Longrightarrow> odd\<iota> (Suc n)"
+ even0: "even 0"
+| evenS: "odd n \<Longrightarrow> even (Suc n)"
+| oddS: "even n \<Longrightarrow> odd (Suc n)"
text {*
Since the predicates @{term even} and @{term odd} are mutually inductive, each
@@ -224,11 +224,11 @@
below @{text "P"} and @{text "Q"}).
*}
-definition "even \<equiv>
+definition "even\<iota> \<equiv>
\<lambda>n. \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m))
\<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> P n"
-definition "odd \<equiv>
+definition "odd\<iota> \<equiv>
\<lambda>n. \<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m))
\<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q n"
@@ -238,11 +238,11 @@
*}
lemma even_induct:
- assumes asm: "even n"
+ assumes "even n"
shows "P 0 \<Longrightarrow>
(\<And>m. Q m \<Longrightarrow> P (Suc m)) \<Longrightarrow> (\<And>m. P m \<Longrightarrow> Q (Suc m)) \<Longrightarrow> P n"
apply(atomize (full))
-apply(cut_tac asm)
+apply(cut_tac prems)
apply(unfold even_def)
apply(drule spec[where x=P])
apply(drule spec[where x=Q])
@@ -263,7 +263,7 @@
apply (unfold odd_def even_def)
apply (rule allI impI)+
proof -
- case (goal1 P)
+ case (goal1 P Q)
have p1: "\<forall>P Q. P 0 \<longrightarrow> (\<forall>m. Q m \<longrightarrow> P (Suc m))
\<longrightarrow> (\<forall>m. P m \<longrightarrow> Q (Suc m)) \<longrightarrow> Q m" by fact
have r1: "P 0" by fact
@@ -303,10 +303,10 @@
*}
lemma accpart_induct:
- assumes asm: "accpart R x"
+ assumes "accpart R x"
shows "(\<And>x. (\<And>y. R y x \<Longrightarrow> P y) \<Longrightarrow> P x) \<Longrightarrow> P x"
apply(atomize (full))
-apply(cut_tac asm)
+apply(cut_tac prems)
apply(unfold accpart_def)
apply(drule spec[where x=P])
apply(assumption)
--- a/CookBook/Package/simple_inductive_package.ML Tue Mar 10 13:20:46 2009 +0000
+++ b/CookBook/Package/simple_inductive_package.ML Wed Mar 11 01:43:28 2009 +0000
@@ -137,24 +137,25 @@
end)
(* @end *)
+fun introductions_tac defs rules preds i ctxt =
+ EVERY1 [ObjectLogic.rulify_tac,
+ K (rewrite_goals_tac defs),
+ REPEAT o (resolve_tac [@{thm allI},@{thm impI}]),
+ subproof1 rules preds i ctxt]
+
+
(* @chunk intro_rules *)
-fun INTROS rules parnames preds defs lthy1 =
+fun introductions rules parnames preds defs lthy1 =
let
val (_, lthy2) = Variable.add_fixes parnames lthy1
fun prove_intro (i, goal) =
Goal.prove lthy2 [] [] goal
- (fn {context = ctxt, ...} =>
- EVERY1
- [ObjectLogic.rulify_tac,
- K (rewrite_goals_tac defs),
- REPEAT o (resolve_tac [@{thm allI},@{thm impI}]),
- subproof1 rules preds i ctxt])
- |> singleton (ProofContext.export lthy2 lthy1)
+ (fn {context, ...} => introductions_tac defs rules preds i context)
+ |> singleton (ProofContext.export lthy2 lthy1)
in
map_index prove_intro rules
end
-
(* @end *)
(* @chunk add_inductive_i *)
@@ -163,7 +164,7 @@
val params' = map (fn (p, T) => Free (Binding.name_of p, T)) params;
val preds' = map (fn ((R, T), _) => list_comb (Free (Binding.name_of R, T), params')) preds;
val Tss = map (binder_types o fastype_of) preds';
- val (ass,rules) = split_list specs;
+ val (ass, rules) = split_list specs; (* FIXME: ass not used? *)
val prednames = map (fst o fst) preds
val syns = map snd preds
@@ -173,7 +174,7 @@
val inducts = inductions rules defs parnames preds' Tss lthy1
- val intros = INTROS rules parnames preds' defs lthy1
+ val intros = introductions rules parnames preds' defs lthy1
val mut_name = space_implode "_" (map (Binding.name_of o fst o fst) preds);
val case_names = map (Binding.name_of o fst o fst) specs
--- a/CookBook/Recipes/Antiquotes.thy Tue Mar 10 13:20:46 2009 +0000
+++ b/CookBook/Recipes/Antiquotes.thy Wed Mar 11 01:43:28 2009 +0000
@@ -36,15 +36,15 @@
*}
+ML {* Pretty.str *}
+
ML%linenosgray{*fun ml_val code_txt = "val _ = " ^ code_txt
-fun output_ml src ctxt code_txt =
+fun output_ml {source = src, context = ctxt, ...} code_txt =
(ML_Context.eval_in (SOME ctxt) false Position.none (ml_val code_txt);
- ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt
- (space_explode "\n" code_txt))
+ ThyOutput.output (map Pretty.str (space_explode "\n" code_txt)))
-val _ = ThyOutput.add_commands
- [("ML_checked", ThyOutput.args (Scan.lift Args.name) output_ml)]*}
+val _ = ThyOutput.antiquotation "ML_checked" (Scan.lift Args.name) output_ml*}
text {*
@@ -53,13 +53,13 @@
is sent to the ML-compiler in the line 4 using the function @{ML ml_val},
which constructs the appropriate ML-expression.
If the code is ``approved'' by the compiler, then the output function @{ML
- "ThyOutput.output_list (fn _ => fn s => Pretty.str s)"} in the next line pretty prints the
+ "ThyOutput.output"} in the next line pretty prints the
code. This function expects that the code is a list of strings where each
string correspond to a line in the output. Therefore the use of
@{ML "(space_explode \"\\n\" txt)" for txt}
- which produces this list according to linebreaks. There are a number of options for antiquotations
- that are observed by @{ML ThyOutput.output_list} when printing the code (including
- @{text "[display]"}, @{text "[quotes]"} and @{text "[source]"}).
+ which produces this list according to linebreaks. There are a number of options
+ for antiquotations that are observed by @{ML ThyOutput.output} when printing the
+ code (including @{text "[display]"} and @{text "[quotes]"}).
\begin{readmore}
For more information about options of antiquotations see \rsccite{sec:antiq}).
@@ -70,14 +70,12 @@
can improve the code above slightly by writing
*}
-ML%linenosgray{*fun output_ml src ctxt (code_txt,pos) =
+ML%linenosgray{*fun output_ml {source = src, context = ctxt, ...} (code_txt,pos) =
(ML_Context.eval_in (SOME ctxt) false pos (ml_val code_txt);
- ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt
- (space_explode "\n" code_txt))
+ ThyOutput.output (map Pretty.str (space_explode "\n" code_txt)))
-val _ = ThyOutput.add_commands
- [("ML_checked", ThyOutput.args
- (Scan.lift (OuterParse.position Args.name)) output_ml)] *}
+val _ = ThyOutput.antiquotation "ML_checked"
+ (Scan.lift (OuterParse.position Args.name)) output_ml *}
text {*
where in Lines 1 and 2 the positional information is properly treated.
@@ -129,19 +127,16 @@
The rest of the code of the antiquotation is
*}
-ML{*fun output_ml_resp src ctxt ((code_txt,pat),pos) =
+ML{*fun output_ml_resp {source = src, context = ctxt, ...} ((code_txt,pat),pos) =
(ML_Context.eval_in (SOME ctxt) false pos (ml_pat (code_txt,pat));
let
val output = (space_explode "\n" code_txt) @ (add_resp_indicator pat)
in
- ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt output
+ ThyOutput.output (map Pretty.str output)
end)
-val _ = ThyOutput.add_commands
- [("ML_resp",
- ThyOutput.args
- (Scan.lift (OuterParse.position (Args.name -- Args.name)))
- output_ml_resp)]*}
+val _ = ThyOutput.antiquotation "ML_resp"
+ (Scan.lift (OuterParse.position (Args.name -- Args.name))) output_ml_resp*}
text {*
This extended antiquotation allows us to write
--- a/CookBook/antiquote_setup.ML Tue Mar 10 13:20:46 2009 +0000
+++ b/CookBook/antiquote_setup.ML Wed Mar 11 01:43:28 2009 +0000
@@ -48,9 +48,9 @@
val output_fn = Chunks.output_list (fn _ => fn s => Pretty.str s)
(* checks and prints open expressions *)
-fun output_ml src node =
+fun output_ml () =
let
- fun output src ctxt ((txt,ovars),pos) =
+ fun output {state: Toplevel.state, source = src, context = ctxt} ((txt,ovars),pos) =
(eval_fn ctxt pos (ml_val_open ovars txt);
output_fn src ctxt (transform_cmts_str txt))
@@ -58,62 +58,63 @@
(Scan.optional (Args.$$$ "for" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [] --
Scan.optional (Args.$$$ "in" |-- OuterParse.!!! (Scan.repeat1 Args.name)) [])))
in
- ThyOutput.args parser output src node
+ ThyOutput.antiquotation "ML" parser output
end
(* checks and prints types and structures *)
-fun output_exp ml src node =
+fun output_exp ml =
let
- fun output src ctxt (txt,pos) =
+ fun output {state: Toplevel.state, source = src, context = ctxt} (txt,pos) =
(eval_fn ctxt pos (ml txt);
output_fn src ctxt (string_explode "" txt))
in
- ThyOutput.args single_arg output src node
+ ThyOutput.antiquotation "ML_type" single_arg output
end
(* checks and expression agains a result pattern *)
-fun output_ml_response src node =
+fun output_ml_response () =
let
- fun output src ctxt ((lhs,pat),pos) =
+ fun output {state: Toplevel.state, source = src, context = ctxt} ((lhs,pat),pos) =
(eval_fn ctxt pos (ml_pat (lhs,pat));
output_fn src ctxt ((string_explode "" lhs) @ (string_explode "> " pat)))
in
- ThyOutput.args two_args output src node
+ ThyOutput.antiquotation "ML_response" two_args output
end
(* checks the expressions, but does not check it against a result pattern *)
-fun output_ml_response_fake src node =
+fun output_ml_response_fake () =
let
- fun output src ctxt ((lhs,pat),pos) =
+ fun output {state: Toplevel.state, source = src, context = ctxt} ((lhs, pat), pos) =
(eval_fn ctxt pos (ml_val lhs);
output_fn src ctxt ((string_explode "" lhs) @ (string_explode "> " pat)))
in
- ThyOutput.args two_args output src node
+ ThyOutput.antiquotation "ML_response_fake" two_args output
end
(* just prints an expression and a result pattern *)
-fun output_ml_response_fake_both src node =
+fun output_ml_response_fake_both () =
let
- fun ouput src ctxt ((lhs,pat), _) =
+ fun ouput {state: Toplevel.state, source = src, context = ctxt} ((lhs,pat), _) =
output_fn src ctxt ((string_explode "" lhs) @ (string_explode "> " pat))
in
- ThyOutput.args two_args ouput src node
+ ThyOutput.antiquotation "ML_response_fake_both" two_args ouput
end
(* checks whether a file exists in the Isabelle distribution *)
-fun check_file_exists src node =
+fun check_file_exists () =
let
fun check txt =
if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then ()
else error ("Source file " ^ (quote txt) ^ " does not exist.")
in
- ThyOutput.args (Scan.lift Args.name)
- (ThyOutput.output (fn _ => fn s => (check s; Pretty.str s))) src node
+ ThyOutput.antiquotation "ML_file" (Scan.lift Args.name)
+ (fn _ => fn s => (check s; ThyOutput.output [Pretty.str s]))
end
(* replaces the official subgoal antiquotation with one *)
(* that is closer to the actual output *)
-fun output_goals src node =
+(*
+fun output_goals {state = node, source: Args.src, context: Proof.context} _ =
let
fun subgoals 0 = ""
| subgoals 1 = "goal (1 subgoal):"
@@ -129,22 +130,22 @@
val {prop, ...} = rep_thm (Proof.get_goal state |> snd |> snd);
val (As, B) = Logic.strip_horn prop;
- val output = (case (length As) of
+ val output' = (case (length As) of
0 => goals
| n => (Pretty.str (subgoals n))::goals)
in
- ThyOutput.args (Scan.succeed ())
- (Chunks.output (fn _ => fn _ => Pretty.chunks output)) src node
+ output
end
+*)
+
-val _ = ThyOutput.add_commands
- [("ML", output_ml),
- ("ML_file", check_file_exists),
- ("ML_response", output_ml_response),
- ("ML_response_fake", output_ml_response_fake),
- ("ML_response_fake_both", output_ml_response_fake_both),
- ("ML_struct", output_exp ml_struct),
- ("ML_type", output_exp ml_type),
- ("subgoals", output_goals)];
+val _ = output_ml ();
+val _ = check_file_exists ();
+val _ = output_ml_response ();
+val _ = output_ml_response_fake ();
+val _ = output_ml_response_fake_both ();
+val _ = output_exp ml_struct;
+val _ = output_exp ml_type;
+(*val _ = output_goals*)
end;
--- a/CookBook/chunks.ML Tue Mar 10 13:20:46 2009 +0000
+++ b/CookBook/chunks.ML Wed Mar 11 01:43:28 2009 +0000
@@ -139,7 +139,7 @@
|| Scan.one not_eof >> ML_Lex.content_of)) #>
fst;
-fun output_chunk src ctxt name =
+fun output_chunk {state: Toplevel.state, source = src, context = ctxt} name =
let
val toks = the_chunk (ProofContext.theory_of ctxt) name;
val (spc, toks') = (case toks of
@@ -164,7 +164,6 @@
output_list (fn _ => fn s => Pretty.str s) src ctxt
end;
-val _ = ThyOutput.add_commands
- [("ML_chunk", ThyOutput.args (Scan.lift Args.name) output_chunk)];
+val _ = ThyOutput.antiquotation "ML_chunk" (Scan.lift Args.name) output_chunk;
end;
Binary file cookbook.pdf has changed