updated some theory primitives, which now depend on auxiliary context;
authorwenzelm
Tue Apr 19 10:50:54 2011 +0200 (2011-04-19)
changeset 424019bfaf6819291
parent 42400 26c8c9cabb24
child 42402 c7139609b67d
updated some theory primitives, which now depend on auxiliary context;
doc-src/IsarImplementation/Thy/Logic.thy
doc-src/IsarImplementation/Thy/Prelim.thy
doc-src/IsarImplementation/Thy/document/Logic.tex
doc-src/IsarImplementation/Thy/document/Prelim.tex
     1.1 --- a/doc-src/IsarImplementation/Thy/Logic.thy	Tue Apr 19 10:37:38 2011 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/Logic.thy	Tue Apr 19 10:50:54 2011 +0200
     1.3 @@ -127,8 +127,10 @@
     1.4    \begin{mldecls}
     1.5    @{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
     1.6    @{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
     1.7 -  @{index_ML Sign.add_types: "(binding * int * mixfix) list -> theory -> theory"} \\
     1.8 -  @{index_ML Sign.add_type_abbrev: "binding * string list * typ -> theory -> theory"} \\
     1.9 +  @{index_ML Sign.add_types: "Proof.context ->
    1.10 +  (binding * int * mixfix) list -> theory -> theory"} \\
    1.11 +  @{index_ML Sign.add_type_abbrev: "Proof.context ->
    1.12 +  binding * string list * typ -> theory -> theory"} \\
    1.13    @{index_ML Sign.primitive_class: "binding * class list -> theory -> theory"} \\
    1.14    @{index_ML Sign.primitive_classrel: "class * class -> theory -> theory"} \\
    1.15    @{index_ML Sign.primitive_arity: "arity -> theory -> theory"} \\
    1.16 @@ -164,13 +166,12 @@
    1.17    \item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether type
    1.18    @{text "\<tau>"} is of sort @{text "s"}.
    1.19  
    1.20 -  \item @{ML Sign.add_types}~@{text "[(\<kappa>, k, mx), \<dots>]"} declares a new
    1.21 -  type constructors @{text "\<kappa>"} with @{text "k"} arguments and
    1.22 +  \item @{ML Sign.add_types}~@{text "ctxt [(\<kappa>, k, mx), \<dots>]"} declares a
    1.23 +  new type constructors @{text "\<kappa>"} with @{text "k"} arguments and
    1.24    optional mixfix syntax.
    1.25  
    1.26 -  \item @{ML Sign.add_type_abbrev}~@{text "(\<kappa>, \<^vec>\<alpha>,
    1.27 -  \<tau>)"} defines a new type abbreviation @{text
    1.28 -  "(\<^vec>\<alpha>)\<kappa> = \<tau>"}.
    1.29 +  \item @{ML Sign.add_type_abbrev}~@{text "ctxt (\<kappa>, \<^vec>\<alpha>, \<tau>)"}
    1.30 +  defines a new type abbreviation @{text "(\<^vec>\<alpha>)\<kappa> = \<tau>"}.
    1.31  
    1.32    \item @{ML Sign.primitive_class}~@{text "(c, [c\<^isub>1, \<dots>,
    1.33    c\<^isub>n])"} declares a new class @{text "c"}, together with class
    1.34 @@ -364,8 +365,8 @@
    1.35    @{index_ML fastype_of: "term -> typ"} \\
    1.36    @{index_ML lambda: "term -> term -> term"} \\
    1.37    @{index_ML betapply: "term * term -> term"} \\
    1.38 -  @{index_ML Sign.declare_const: "(binding * typ) * mixfix ->
    1.39 -  theory -> term * theory"} \\
    1.40 +  @{index_ML Sign.declare_const: "Proof.context ->
    1.41 +  (binding * typ) * mixfix -> theory -> term * theory"} \\
    1.42    @{index_ML Sign.add_abbrev: "string -> binding * term ->
    1.43    theory -> (term * term) * theory"} \\
    1.44    @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
    1.45 @@ -412,9 +413,8 @@
    1.46    "t u"}, with topmost @{text "\<beta>"}-conversion if @{text "t"} is an
    1.47    abstraction.
    1.48  
    1.49 -  \item @{ML Sign.declare_const}~@{text "((c, \<sigma>), mx)"}
    1.50 -  declares a new constant @{text "c :: \<sigma>"} with optional mixfix
    1.51 -  syntax.
    1.52 +  \item @{ML Sign.declare_const}~@{text "ctxt ((c, \<sigma>), mx)"} declares
    1.53 +  a new constant @{text "c :: \<sigma>"} with optional mixfix syntax.
    1.54  
    1.55    \item @{ML Sign.add_abbrev}~@{text "print_mode (c, t)"}
    1.56    introduces a new term abbreviation @{text "c \<equiv> t"}.
    1.57 @@ -640,15 +640,16 @@
    1.58    @{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\
    1.59    @{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
    1.60    @{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
    1.61 -  @{index_ML Thm.add_axiom: "binding * term -> theory -> (string * thm) * theory"} \\
    1.62 +  @{index_ML Thm.add_axiom: "Proof.context ->
    1.63 +  binding * term -> theory -> (string * thm) * theory"} \\
    1.64    @{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory ->
    1.65    (string * ('a -> thm)) * theory"} \\
    1.66 -  @{index_ML Thm.add_def: "bool -> bool -> binding * term -> theory ->
    1.67 -  (string * thm) * theory"} \\
    1.68 +  @{index_ML Thm.add_def: "Proof.context -> bool -> bool ->
    1.69 +  binding * term -> theory -> (string * thm) * theory"} \\
    1.70    \end{mldecls}
    1.71    \begin{mldecls}
    1.72 -  @{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list ->
    1.73 -  theory -> theory"} \\
    1.74 +  @{index_ML Theory.add_deps: "Proof.context -> string ->
    1.75 +  string * typ -> (string * typ) list -> theory -> theory"} \\
    1.76    \end{mldecls}
    1.77  
    1.78    \begin{description}
    1.79 @@ -696,7 +697,7 @@
    1.80    term variables.  Note that the types in @{text "\<^vec>x\<^isub>\<tau>"}
    1.81    refer to the instantiated versions.
    1.82  
    1.83 -  \item @{ML Thm.add_axiom}~@{text "(name, A) thy"} declares an
    1.84 +  \item @{ML Thm.add_axiom}~@{text "ctxt (name, A)"} declares an
    1.85    arbitrary proposition as axiom, and retrieves it as a theorem from
    1.86    the resulting theory, cf.\ @{text "axiom"} in
    1.87    \figref{fig:prim-rules}.  Note that the low-level representation in
    1.88 @@ -706,17 +707,17 @@
    1.89    oracle rule, essentially generating arbitrary axioms on the fly,
    1.90    cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
    1.91  
    1.92 -  \item @{ML Thm.add_def}~@{text "unchecked overloaded (name, c
    1.93 +  \item @{ML Thm.add_def}~@{text "ctxt unchecked overloaded (name, c
    1.94    \<^vec>x \<equiv> t)"} states a definitional axiom for an existing constant
    1.95    @{text "c"}.  Dependencies are recorded via @{ML Theory.add_deps},
    1.96    unless the @{text "unchecked"} option is set.  Note that the
    1.97    low-level representation in the axiom table may differ slightly from
    1.98    the returned theorem.
    1.99  
   1.100 -  \item @{ML Theory.add_deps}~@{text "name c\<^isub>\<tau>
   1.101 -  \<^vec>d\<^isub>\<sigma>"} declares dependencies of a named specification
   1.102 -  for constant @{text "c\<^isub>\<tau>"}, relative to existing
   1.103 -  specifications for constants @{text "\<^vec>d\<^isub>\<sigma>"}.
   1.104 +  \item @{ML Theory.add_deps}~@{text "ctxt name c\<^isub>\<tau> \<^vec>d\<^isub>\<sigma>"}
   1.105 +  declares dependencies of a named specification for constant @{text
   1.106 +  "c\<^isub>\<tau>"}, relative to existing specifications for constants @{text
   1.107 +  "\<^vec>d\<^isub>\<sigma>"}.
   1.108  
   1.109    \end{description}
   1.110  *}
     2.1 --- a/doc-src/IsarImplementation/Thy/Prelim.thy	Tue Apr 19 10:37:38 2011 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Tue Apr 19 10:50:54 2011 +0200
     2.3 @@ -1109,8 +1109,8 @@
     2.4    @{index_ML_type Name_Space.T} \\
     2.5    @{index_ML Name_Space.empty: "string -> Name_Space.T"} \\
     2.6    @{index_ML Name_Space.merge: "Name_Space.T * Name_Space.T -> Name_Space.T"} \\
     2.7 -  @{index_ML Name_Space.declare: "bool -> Name_Space.naming -> binding -> Name_Space.T ->
     2.8 -  string * Name_Space.T"} \\
     2.9 +  @{index_ML Name_Space.declare: "Proof.context -> bool ->
    2.10 +  Name_Space.naming -> binding -> Name_Space.T -> string * Name_Space.T"} \\
    2.11    @{index_ML Name_Space.intern: "Name_Space.T -> string -> string"} \\
    2.12    @{index_ML Name_Space.extern: "Proof.context -> Name_Space.T -> string -> string"} \\
    2.13    @{index_ML Name_Space.is_concealed: "Name_Space.T -> string -> bool"}
    2.14 @@ -1173,7 +1173,7 @@
    2.15    (\secref{sec:context-data}); @{text "kind"} is a formal comment
    2.16    to characterize the purpose of a name space.
    2.17  
    2.18 -  \item @{ML Name_Space.declare}~@{text "strict naming bindings
    2.19 +  \item @{ML Name_Space.declare}~@{text "ctxt strict naming bindings
    2.20    space"} enters a name binding as fully qualified internal name into
    2.21    the name space, with external accesses determined by the naming
    2.22    policy.
     3.1 --- a/doc-src/IsarImplementation/Thy/document/Logic.tex	Tue Apr 19 10:37:38 2011 +0200
     3.2 +++ b/doc-src/IsarImplementation/Thy/document/Logic.tex	Tue Apr 19 10:50:54 2011 +0200
     3.3 @@ -138,8 +138,10 @@
     3.4    \begin{mldecls}
     3.5    \indexdef{}{ML}{Sign.subsort}\verb|Sign.subsort: theory -> sort * sort -> bool| \\
     3.6    \indexdef{}{ML}{Sign.of\_sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\
     3.7 -  \indexdef{}{ML}{Sign.add\_types}\verb|Sign.add_types: (binding * int * mixfix) list -> theory -> theory| \\
     3.8 -  \indexdef{}{ML}{Sign.add\_type\_abbrev}\verb|Sign.add_type_abbrev: binding * string list * typ -> theory -> theory| \\
     3.9 +  \indexdef{}{ML}{Sign.add\_types}\verb|Sign.add_types: Proof.context ->|\isasep\isanewline%
    3.10 +\verb|  (binding * int * mixfix) list -> theory -> theory| \\
    3.11 +  \indexdef{}{ML}{Sign.add\_type\_abbrev}\verb|Sign.add_type_abbrev: Proof.context ->|\isasep\isanewline%
    3.12 +\verb|  binding * string list * typ -> theory -> theory| \\
    3.13    \indexdef{}{ML}{Sign.primitive\_class}\verb|Sign.primitive_class: binding * class list -> theory -> theory| \\
    3.14    \indexdef{}{ML}{Sign.primitive\_classrel}\verb|Sign.primitive_classrel: class * class -> theory -> theory| \\
    3.15    \indexdef{}{ML}{Sign.primitive\_arity}\verb|Sign.primitive_arity: arity -> theory -> theory| \\
    3.16 @@ -172,11 +174,12 @@
    3.17    \item \verb|Sign.of_sort|~\isa{thy\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}} tests whether type
    3.18    \isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} is of sort \isa{s}.
    3.19  
    3.20 -  \item \verb|Sign.add_types|~\isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{2C}{\isacharcomma}}\ k{\isaliteral{2C}{\isacharcomma}}\ mx{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{5D}{\isacharbrackright}}} declares a new
    3.21 -  type constructors \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} with \isa{k} arguments and
    3.22 +  \item \verb|Sign.add_types|~\isa{ctxt\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{2C}{\isacharcomma}}\ k{\isaliteral{2C}{\isacharcomma}}\ mx{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{5D}{\isacharbrackright}}} declares a
    3.23 +  new type constructors \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} with \isa{k} arguments and
    3.24    optional mixfix syntax.
    3.25  
    3.26 -  \item \verb|Sign.add_type_abbrev|~\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}} defines a new type abbreviation \isa{{\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}}.
    3.27 +  \item \verb|Sign.add_type_abbrev|~\isa{ctxt\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{2C}{\isacharcomma}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{29}{\isacharparenright}}}
    3.28 +  defines a new type abbreviation \isa{{\isaliteral{28}{\isacharparenleft}}\isaliteral{5C3C5E7665633E}{}\isactrlvec {\isaliteral{5C3C616C7068613E}{\isasymalpha}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C7461753E}{\isasymtau}}}.
    3.29  
    3.30    \item \verb|Sign.primitive_class|~\isa{{\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5B}{\isacharbrackleft}}c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{29}{\isacharparenright}}} declares a new class \isa{c}, together with class
    3.31    relations \isa{c\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub i}, for \isa{i\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ n}.
    3.32 @@ -386,8 +389,8 @@
    3.33    \indexdef{}{ML}{fastype\_of}\verb|fastype_of: term -> typ| \\
    3.34    \indexdef{}{ML}{lambda}\verb|lambda: term -> term -> term| \\
    3.35    \indexdef{}{ML}{betapply}\verb|betapply: term * term -> term| \\
    3.36 -  \indexdef{}{ML}{Sign.declare\_const}\verb|Sign.declare_const: (binding * typ) * mixfix ->|\isasep\isanewline%
    3.37 -\verb|  theory -> term * theory| \\
    3.38 +  \indexdef{}{ML}{Sign.declare\_const}\verb|Sign.declare_const: Proof.context ->|\isasep\isanewline%
    3.39 +\verb|  (binding * typ) * mixfix -> theory -> term * theory| \\
    3.40    \indexdef{}{ML}{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> binding * term ->|\isasep\isanewline%
    3.41  \verb|  theory -> (term * term) * theory| \\
    3.42    \indexdef{}{ML}{Sign.const\_typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
    3.43 @@ -426,9 +429,8 @@
    3.44    \item \verb|betapply|~\isa{{\isaliteral{28}{\isacharparenleft}}t{\isaliteral{2C}{\isacharcomma}}\ u{\isaliteral{29}{\isacharparenright}}} produces an application \isa{t\ u}, with topmost \isa{{\isaliteral{5C3C626574613E}{\isasymbeta}}}-conversion if \isa{t} is an
    3.45    abstraction.
    3.46  
    3.47 -  \item \verb|Sign.declare_const|~\isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ mx{\isaliteral{29}{\isacharparenright}}}
    3.48 -  declares a new constant \isa{c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} with optional mixfix
    3.49 -  syntax.
    3.50 +  \item \verb|Sign.declare_const|~\isa{ctxt\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{2C}{\isacharcomma}}\ mx{\isaliteral{29}{\isacharparenright}}} declares
    3.51 +  a new constant \isa{c\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} with optional mixfix syntax.
    3.52  
    3.53    \item \verb|Sign.add_abbrev|~\isa{print{\isaliteral{5F}{\isacharunderscore}}mode\ {\isaliteral{28}{\isacharparenleft}}c{\isaliteral{2C}{\isacharcomma}}\ t{\isaliteral{29}{\isacharparenright}}}
    3.54    introduces a new term abbreviation \isa{c\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t}.
    3.55 @@ -673,15 +675,16 @@
    3.56    \indexdef{}{ML}{Thm.implies\_elim}\verb|Thm.implies_elim: thm -> thm -> thm| \\
    3.57    \indexdef{}{ML}{Thm.generalize}\verb|Thm.generalize: string list * string list -> int -> thm -> thm| \\
    3.58    \indexdef{}{ML}{Thm.instantiate}\verb|Thm.instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm| \\
    3.59 -  \indexdef{}{ML}{Thm.add\_axiom}\verb|Thm.add_axiom: binding * term -> theory -> (string * thm) * theory| \\
    3.60 +  \indexdef{}{ML}{Thm.add\_axiom}\verb|Thm.add_axiom: Proof.context ->|\isasep\isanewline%
    3.61 +\verb|  binding * term -> theory -> (string * thm) * theory| \\
    3.62    \indexdef{}{ML}{Thm.add\_oracle}\verb|Thm.add_oracle: binding * ('a -> cterm) -> theory ->|\isasep\isanewline%
    3.63  \verb|  (string * ('a -> thm)) * theory| \\
    3.64 -  \indexdef{}{ML}{Thm.add\_def}\verb|Thm.add_def: bool -> bool -> binding * term -> theory ->|\isasep\isanewline%
    3.65 -\verb|  (string * thm) * theory| \\
    3.66 +  \indexdef{}{ML}{Thm.add\_def}\verb|Thm.add_def: Proof.context -> bool -> bool ->|\isasep\isanewline%
    3.67 +\verb|  binding * term -> theory -> (string * thm) * theory| \\
    3.68    \end{mldecls}
    3.69    \begin{mldecls}
    3.70 -  \indexdef{}{ML}{Theory.add\_deps}\verb|Theory.add_deps: string -> string * typ -> (string * typ) list ->|\isasep\isanewline%
    3.71 -\verb|  theory -> theory| \\
    3.72 +  \indexdef{}{ML}{Theory.add\_deps}\verb|Theory.add_deps: Proof.context -> string ->|\isasep\isanewline%
    3.73 +\verb|  string * typ -> (string * typ) list -> theory -> theory| \\
    3.74    \end{mldecls}
    3.75  
    3.76    \begin{description}
    3.77 @@ -726,7 +729,7 @@
    3.78    term variables.  Note that the types in \isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}}
    3.79    refer to the instantiated versions.
    3.80  
    3.81 -  \item \verb|Thm.add_axiom|~\isa{{\isaliteral{28}{\isacharparenleft}}name{\isaliteral{2C}{\isacharcomma}}\ A{\isaliteral{29}{\isacharparenright}}\ thy} declares an
    3.82 +  \item \verb|Thm.add_axiom|~\isa{ctxt\ {\isaliteral{28}{\isacharparenleft}}name{\isaliteral{2C}{\isacharcomma}}\ A{\isaliteral{29}{\isacharparenright}}} declares an
    3.83    arbitrary proposition as axiom, and retrieves it as a theorem from
    3.84    the resulting theory, cf.\ \isa{axiom} in
    3.85    \figref{fig:prim-rules}.  Note that the low-level representation in
    3.86 @@ -736,15 +739,14 @@
    3.87    oracle rule, essentially generating arbitrary axioms on the fly,
    3.88    cf.\ \isa{axiom} in \figref{fig:prim-rules}.
    3.89  
    3.90 -  \item \verb|Thm.add_def|~\isa{unchecked\ overloaded\ {\isaliteral{28}{\isacharparenleft}}name{\isaliteral{2C}{\isacharcomma}}\ c\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{29}{\isacharparenright}}} states a definitional axiom for an existing constant
    3.91 +  \item \verb|Thm.add_def|~\isa{ctxt\ unchecked\ overloaded\ {\isaliteral{28}{\isacharparenleft}}name{\isaliteral{2C}{\isacharcomma}}\ c\ \isaliteral{5C3C5E7665633E}{}\isactrlvec x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ t{\isaliteral{29}{\isacharparenright}}} states a definitional axiom for an existing constant
    3.92    \isa{c}.  Dependencies are recorded via \verb|Theory.add_deps|,
    3.93    unless the \isa{unchecked} option is set.  Note that the
    3.94    low-level representation in the axiom table may differ slightly from
    3.95    the returned theorem.
    3.96  
    3.97 -  \item \verb|Theory.add_deps|~\isa{name\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec d\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7369676D613E}{\isasymsigma}}} declares dependencies of a named specification
    3.98 -  for constant \isa{c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}}, relative to existing
    3.99 -  specifications for constants \isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec d\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7369676D613E}{\isasymsigma}}}.
   3.100 +  \item \verb|Theory.add_deps|~\isa{ctxt\ name\ c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}\ \isaliteral{5C3C5E7665633E}{}\isactrlvec d\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7369676D613E}{\isasymsigma}}}
   3.101 +  declares dependencies of a named specification for constant \isa{c\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7461753E}{\isasymtau}}}, relative to existing specifications for constants \isa{\isaliteral{5C3C5E7665633E}{}\isactrlvec d\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isaliteral{5C3C7369676D613E}{\isasymsigma}}}.
   3.102  
   3.103    \end{description}%
   3.104  \end{isamarkuptext}%
     4.1 --- a/doc-src/IsarImplementation/Thy/document/Prelim.tex	Tue Apr 19 10:37:38 2011 +0200
     4.2 +++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex	Tue Apr 19 10:50:54 2011 +0200
     4.3 @@ -1607,8 +1607,8 @@
     4.4    \indexdef{}{ML type}{Name\_Space.T}\verb|type Name_Space.T| \\
     4.5    \indexdef{}{ML}{Name\_Space.empty}\verb|Name_Space.empty: string -> Name_Space.T| \\
     4.6    \indexdef{}{ML}{Name\_Space.merge}\verb|Name_Space.merge: Name_Space.T * Name_Space.T -> Name_Space.T| \\
     4.7 -  \indexdef{}{ML}{Name\_Space.declare}\verb|Name_Space.declare: bool -> Name_Space.naming -> binding -> Name_Space.T ->|\isasep\isanewline%
     4.8 -\verb|  string * Name_Space.T| \\
     4.9 +  \indexdef{}{ML}{Name\_Space.declare}\verb|Name_Space.declare: Proof.context -> bool ->|\isasep\isanewline%
    4.10 +\verb|  Name_Space.naming -> binding -> Name_Space.T -> string * Name_Space.T| \\
    4.11    \indexdef{}{ML}{Name\_Space.intern}\verb|Name_Space.intern: Name_Space.T -> string -> string| \\
    4.12    \indexdef{}{ML}{Name\_Space.extern}\verb|Name_Space.extern: Proof.context -> Name_Space.T -> string -> string| \\
    4.13    \indexdef{}{ML}{Name\_Space.is\_concealed}\verb|Name_Space.is_concealed: Name_Space.T -> string -> bool|
    4.14 @@ -1667,7 +1667,7 @@
    4.15    (\secref{sec:context-data}); \isa{kind} is a formal comment
    4.16    to characterize the purpose of a name space.
    4.17  
    4.18 -  \item \verb|Name_Space.declare|~\isa{strict\ naming\ bindings\ space} enters a name binding as fully qualified internal name into
    4.19 +  \item \verb|Name_Space.declare|~\isa{ctxt\ strict\ naming\ bindings\ space} enters a name binding as fully qualified internal name into
    4.20    the name space, with external accesses determined by the naming
    4.21    policy.
    4.22