Added Fred's example on modifying the proof context for parsing.
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
Isabelle_DOF/Isabelle_DOF/master This commit looks good
Details
This commit is contained in:
parent
b863a0178f
commit
cc787cb9f1
|
@ -602,6 +602,36 @@ fun mk_meta_eq (t, u) = meta_eq_const (fastype_of t) $ t $ u;
|
||||||
|
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
subsection\<open>Another Approach for Typed Parsing\<close>
|
||||||
|
|
||||||
|
text\<open>Another example for influencing @{ML "Syntax.read_term"} by modifying
|
||||||
|
the @{ML_type "Proof.context"}: \<close>
|
||||||
|
|
||||||
|
definition "zz = ()"
|
||||||
|
ML\<open>@{term zz}\<close> (* So : @(term "zz"} is now a constant*)
|
||||||
|
ML\<open>val Free ("zz", ty) = Proof_Context.add_fixes
|
||||||
|
[(@{binding "zz"}, SOME @{typ nat}, NoSyn)] @{context}
|
||||||
|
|> (fn (S, ctxt) => (writeln (String.concat S);
|
||||||
|
Syntax.read_term ctxt "zz"));
|
||||||
|
(* So : @(term "zz"} is here a free variable. *) \<close>
|
||||||
|
ML\<open>@{term zz}\<close> (* So : @(term "zz"} is now a constant again.*)
|
||||||
|
locale Z =
|
||||||
|
fixes zz :: nat
|
||||||
|
begin
|
||||||
|
ML\<open>@{term "(zz)"}\<close>
|
||||||
|
end
|
||||||
|
|
||||||
|
lemma True
|
||||||
|
proof - fix a :: nat
|
||||||
|
show True
|
||||||
|
ML_prf \<open>@{term a}\<close>
|
||||||
|
term a
|
||||||
|
oops
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
subsection*[t233::technical]\<open> Theories and the Signature API\<close>
|
subsection*[t233::technical]\<open> Theories and the Signature API\<close>
|
||||||
ML\<open>
|
ML\<open>
|
||||||
Sign.tsig_of : theory -> Type.tsig;
|
Sign.tsig_of : theory -> Type.tsig;
|
||||||
|
|
|
@ -42,7 +42,9 @@ doc_class D = B +
|
||||||
|
|
||||||
doc_class E = D +
|
doc_class E = D +
|
||||||
x :: "string" <= "''qed''" (* overriding default *)
|
x :: "string" <= "''qed''" (* overriding default *)
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
doc_class F =
|
doc_class F =
|
||||||
properties :: "term list"
|
properties :: "term list"
|
||||||
r :: "thm list"
|
r :: "thm list"
|
||||||
|
|
|
@ -30,7 +30,18 @@ val {docobj_tab={tab = docitem_tab, ...},docclass_tab, ISA_transformer_tab, moni
|
||||||
Symtab.dest docitem_tab;
|
Symtab.dest docitem_tab;
|
||||||
Symtab.dest docclass_tab;
|
Symtab.dest docclass_tab;
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
|
|
||||||
|
ML\<open>
|
||||||
|
fun fac x = if x = 0 then 1 else x * (fac(x -1));
|
||||||
|
fac 3;
|
||||||
|
\<close>
|
||||||
|
|
||||||
|
ML\<open>
|
||||||
|
open Thm;
|
||||||
|
\<close>
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
text\<open>A text item containing standard theorem antiquotations and complex meta-information.\<close>
|
text\<open>A text item containing standard theorem antiquotations and complex meta-information.\<close>
|
||||||
(* crashes in batch mode ...
|
(* crashes in batch mode ...
|
||||||
|
|
|
@ -29,7 +29,7 @@ section*[a::A, x = "3"] \<open> Lorem ipsum dolor sit amet, ... \<close>
|
||||||
text*[c1::C, x = "''beta''"] \<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ... \<close>
|
text*[c1::C, x = "''beta''"] \<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ... \<close>
|
||||||
|
|
||||||
text*[d::D, a1 = "X3"] \<open> ... phasellus amet id massa nunc, pede suscipit repellendus,
|
text*[d::D, a1 = "X3"] \<open> ... phasellus amet id massa nunc, pede suscipit repellendus,
|
||||||
... @{docitem "c1"} @{thm "refl"} \<close>
|
... @{C "c1"} @{thm "refl"} \<close>
|
||||||
|
|
||||||
|
|
||||||
update_instance*[d::D, a1 := X2]
|
update_instance*[d::D, a1 := X2]
|
||||||
|
|
Loading…
Reference in New Issue