--- a/doc-src/IsarImplementation/Thy/Logic.thy Wed Mar 28 10:44:04 2012 +0200
+++ b/doc-src/IsarImplementation/Thy/Logic.thy Wed Mar 28 11:40:12 2012 +0200
@@ -127,8 +127,7 @@
\begin{mldecls}
@{index_ML Sign.subsort: "theory -> sort * sort -> bool"} \\
@{index_ML Sign.of_sort: "theory -> typ * sort -> bool"} \\
- @{index_ML Sign.add_types: "Proof.context ->
- (binding * int * mixfix) list -> theory -> theory"} \\
+ @{index_ML Sign.add_type: "Proof.context -> binding * int * mixfix -> theory -> theory"} \\
@{index_ML Sign.add_type_abbrev: "Proof.context ->
binding * string list * typ -> theory -> theory"} \\
@{index_ML Sign.primitive_class: "binding * class list -> theory -> theory"} \\
@@ -166,7 +165,7 @@
\item @{ML Sign.of_sort}~@{text "thy (\<tau>, s)"} tests whether type
@{text "\<tau>"} is of sort @{text "s"}.
- \item @{ML Sign.add_types}~@{text "ctxt [(\<kappa>, k, mx), \<dots>]"} declares a
+ \item @{ML Sign.add_type}~@{text "ctxt (\<kappa>, k, mx)"} declares a
new type constructors @{text "\<kappa>"} with @{text "k"} arguments and
optional mixfix syntax.
--- a/doc-src/IsarImplementation/Thy/Prelim.thy Wed Mar 28 10:44:04 2012 +0200
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy Wed Mar 28 11:40:12 2012 +0200
@@ -1106,8 +1106,8 @@
@{index_ML_type Name_Space.T} \\
@{index_ML Name_Space.empty: "string -> Name_Space.T"} \\
@{index_ML Name_Space.merge: "Name_Space.T * Name_Space.T -> Name_Space.T"} \\
- @{index_ML Name_Space.declare: "Proof.context -> bool ->
- Name_Space.naming -> binding -> Name_Space.T -> string * Name_Space.T"} \\
+ @{index_ML Name_Space.declare: "Context.generic -> bool ->
+ binding -> Name_Space.T -> string * Name_Space.T"} \\
@{index_ML Name_Space.intern: "Name_Space.T -> string -> string"} \\
@{index_ML Name_Space.extern: "Proof.context -> Name_Space.T -> string -> string"} \\
@{index_ML Name_Space.is_concealed: "Name_Space.T -> string -> bool"}
@@ -1170,10 +1170,9 @@
(\secref{sec:context-data}); @{text "kind"} is a formal comment
to characterize the purpose of a name space.
- \item @{ML Name_Space.declare}~@{text "ctxt strict naming bindings
+ \item @{ML Name_Space.declare}~@{text "context strict binding
space"} enters a name binding as fully qualified internal name into
- the name space, with external accesses determined by the naming
- policy.
+ the name space, using the naming of the context.
\item @{ML Name_Space.intern}~@{text "space name"} internalizes a
(partially qualified) external name.
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex Wed Mar 28 10:44:04 2012 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex Wed Mar 28 11:40:12 2012 +0200
@@ -138,8 +138,7 @@
\begin{mldecls}
\indexdef{}{ML}{Sign.subsort}\verb|Sign.subsort: theory -> sort * sort -> bool| \\
\indexdef{}{ML}{Sign.of\_sort}\verb|Sign.of_sort: theory -> typ * sort -> bool| \\
- \indexdef{}{ML}{Sign.add\_types}\verb|Sign.add_types: Proof.context ->|\isasep\isanewline%
-\verb| (binding * int * mixfix) list -> theory -> theory| \\
+ \indexdef{}{ML}{Sign.add\_type}\verb|Sign.add_type: Proof.context -> binding * int * mixfix -> theory -> theory| \\
\indexdef{}{ML}{Sign.add\_type\_abbrev}\verb|Sign.add_type_abbrev: Proof.context ->|\isasep\isanewline%
\verb| binding * string list * typ -> theory -> theory| \\
\indexdef{}{ML}{Sign.primitive\_class}\verb|Sign.primitive_class: binding * class list -> theory -> theory| \\
@@ -174,7 +173,7 @@
\item \verb|Sign.of_sort|~\isa{thy\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C7461753E}{\isasymtau}}{\isaliteral{2C}{\isacharcomma}}\ s{\isaliteral{29}{\isacharparenright}}} tests whether type
\isa{{\isaliteral{5C3C7461753E}{\isasymtau}}} is of sort \isa{s}.
- \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
+ \item \verb|Sign.add_type|~\isa{ctxt\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6B617070613E}{\isasymkappa}}{\isaliteral{2C}{\isacharcomma}}\ k{\isaliteral{2C}{\isacharcomma}}\ mx{\isaliteral{29}{\isacharparenright}}} declares a
new type constructors \isa{{\isaliteral{5C3C6B617070613E}{\isasymkappa}}} with \isa{k} arguments and
optional mixfix syntax.
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Wed Mar 28 10:44:04 2012 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Wed Mar 28 11:40:12 2012 +0200
@@ -1617,8 +1617,8 @@
\indexdef{}{ML type}{Name\_Space.T}\verb|type Name_Space.T| \\
\indexdef{}{ML}{Name\_Space.empty}\verb|Name_Space.empty: string -> Name_Space.T| \\
\indexdef{}{ML}{Name\_Space.merge}\verb|Name_Space.merge: Name_Space.T * Name_Space.T -> Name_Space.T| \\
- \indexdef{}{ML}{Name\_Space.declare}\verb|Name_Space.declare: Proof.context -> bool ->|\isasep\isanewline%
-\verb| Name_Space.naming -> binding -> Name_Space.T -> string * Name_Space.T| \\
+ \indexdef{}{ML}{Name\_Space.declare}\verb|Name_Space.declare: Context.generic -> bool ->|\isasep\isanewline%
+\verb| binding -> Name_Space.T -> string * Name_Space.T| \\
\indexdef{}{ML}{Name\_Space.intern}\verb|Name_Space.intern: Name_Space.T -> string -> string| \\
\indexdef{}{ML}{Name\_Space.extern}\verb|Name_Space.extern: Proof.context -> Name_Space.T -> string -> string| \\
\indexdef{}{ML}{Name\_Space.is\_concealed}\verb|Name_Space.is_concealed: Name_Space.T -> string -> bool|
@@ -1677,9 +1677,8 @@
(\secref{sec:context-data}); \isa{kind} is a formal comment
to characterize the purpose of a name space.
- \item \verb|Name_Space.declare|~\isa{ctxt\ strict\ naming\ bindings\ space} enters a name binding as fully qualified internal name into
- the name space, with external accesses determined by the naming
- policy.
+ \item \verb|Name_Space.declare|~\isa{context\ strict\ binding\ space} enters a name binding as fully qualified internal name into
+ the name space, using the naming of the context.
\item \verb|Name_Space.intern|~\isa{space\ name} internalizes a
(partially qualified) external name.
--- a/etc/settings Wed Mar 28 10:44:04 2012 +0200
+++ b/etc/settings Wed Mar 28 11:40:12 2012 +0200
@@ -1,11 +1,11 @@
# -*- shell-script -*- :mode=shellscript:
#
-# Isabelle settings -- site defaults.
+# Isabelle settings -- distribution defaults.
#
# Important notes:
-# * See the system manual for explanations on Isabelle settings
+# * See the "system" manual for explanations on Isabelle settings
# * DO NOT EDIT the repository copy of this file!
-# * DO NOT COPY this file into your personal isabelle directory!
+# * DO NOT COPY this file into your ~/.isabelle directory!
###
### ML compiler settings (ESSENTIAL!)