From cc787cb9f1b969400b5ecee99f6697c1d3feeee9 Mon Sep 17 00:00:00 2001
From: bu <wolff@lri.fr>
Date: Tue, 1 Oct 2019 17:57:26 +0200
Subject: [PATCH] Added Fred's example on modifying the proof context for
 parsing.

---
 .../TR_MyCommentedIsabelle.thy                | 30 +++++++++++++++++++
 src/ontologies/Conceptual/Conceptual.thy      |  4 ++-
 src/tests/Attributes.thy                      | 13 +++++++-
 src/tests/Concept_Example.thy                 |  2 +-
 4 files changed, 46 insertions(+), 3 deletions(-)

diff --git a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy
index a352c3ae..6b5f3456 100644
--- a/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy
+++ b/examples/technical_report/TR_my_commented_isabelle/TR_MyCommentedIsabelle.thy
@@ -602,6 +602,36 @@ fun mk_meta_eq (t, u) = meta_eq_const (fastype_of t) $ t $ u;
 
 \<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>  
 ML\<open>
 Sign.tsig_of : theory -> Type.tsig;
diff --git a/src/ontologies/Conceptual/Conceptual.thy b/src/ontologies/Conceptual/Conceptual.thy
index e49b9f09..868558fe 100644
--- a/src/ontologies/Conceptual/Conceptual.thy
+++ b/src/ontologies/Conceptual/Conceptual.thy
@@ -42,7 +42,9 @@ doc_class D = B +
 
 doc_class E = D +
    x :: "string"              <= "''qed''"  (* overriding default *)
-   
+
+
+
 doc_class F  = 
    properties :: "term list"
    r          :: "thm list"
diff --git a/src/tests/Attributes.thy b/src/tests/Attributes.thy
index bf76d1aa..aa2798ac 100644
--- a/src/tests/Attributes.thy
+++ b/src/tests/Attributes.thy
@@ -30,7 +30,18 @@ val {docobj_tab={tab = docitem_tab, ...},docclass_tab, ISA_transformer_tab, moni
 Symtab.dest docitem_tab;
 Symtab.dest docclass_tab;
 \<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>
 (* crashes in batch mode ... 
diff --git a/src/tests/Concept_Example.thy b/src/tests/Concept_Example.thy
index e1d6322b..a6e18fce 100644
--- a/src/tests/Concept_Example.thy
+++ b/src/tests/Concept_Example.thy
@@ -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*[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]