--- a/doc-src/IsarImplementation/Thy/Logic.thy Sun Oct 25 21:35:46 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/Logic.thy Mon Oct 26 08:54:20 2009 +0100
@@ -322,9 +322,9 @@
@{index_ML fastype_of: "term -> typ"} \\
@{index_ML lambda: "term -> term -> term"} \\
@{index_ML betapply: "term * term -> term"} \\
- @{index_ML Sign.declare_const: "Properties.T -> (binding * typ) * mixfix ->
+ @{index_ML Sign.declare_const: "(binding * typ) * mixfix ->
theory -> term * theory"} \\
- @{index_ML Sign.add_abbrev: "string -> Properties.T -> binding * term ->
+ @{index_ML Sign.add_abbrev: "string -> binding * term ->
theory -> (term * term) * theory"} \\
@{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
@{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
@@ -370,11 +370,11 @@
"t u"}, with topmost @{text "\<beta>"}-conversion if @{text "t"} is an
abstraction.
- \item @{ML Sign.declare_const}~@{text "properties ((c, \<sigma>), mx)"}
+ \item @{ML Sign.declare_const}~@{text "((c, \<sigma>), mx)"}
declares a new constant @{text "c :: \<sigma>"} with optional mixfix
syntax.
- \item @{ML Sign.add_abbrev}~@{text "print_mode properties (c, t)"}
+ \item @{ML Sign.add_abbrev}~@{text "print_mode (c, t)"}
introduces a new term abbreviation @{text "c \<equiv> t"}.
\item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} and @{ML
--- a/doc-src/IsarImplementation/Thy/ML.thy Sun Oct 25 21:35:46 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/ML.thy Mon Oct 26 08:54:20 2009 +0100
@@ -317,7 +317,7 @@
a theory by constant declararion and primitive definitions:
\smallskip\begin{mldecls}
- @{ML "Sign.declare_const: Properties.T -> (binding * typ) * mixfix
+ @{ML "Sign.declare_const: (binding * typ) * mixfix
-> theory -> term * theory"} \\
@{ML "Thm.add_def: bool -> bool -> binding * term -> theory -> thm * theory"}
\end{mldecls}
@@ -329,7 +329,7 @@
\smallskip\begin{mldecls}
@{ML "(fn (t, thy) => Thm.add_def false false
(Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})) thy)
- (Sign.declare_const []
+ (Sign.declare_const
((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn) thy)"}
\end{mldecls}
@@ -344,7 +344,7 @@
\smallskip\begin{mldecls}
@{ML "thy
-|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
+|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
|> (fn (t, thy) => thy
|> Thm.add_def false false
(Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))"}
@@ -368,7 +368,7 @@
\smallskip\begin{mldecls}
@{ML "thy
-|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
+|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
|-> (fn t => Thm.add_def false false
(Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
"}
@@ -378,7 +378,7 @@
\smallskip\begin{mldecls}
@{ML "thy
-|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
+|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
|>> (fn t => Logic.mk_equals (t, @{term \"%x. x\"}))
|-> (fn def => Thm.add_def false false (Binding.name \"bar_def\", def))
"}
@@ -389,7 +389,7 @@
\smallskip\begin{mldecls}
@{ML "thy
-|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
+|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
||> Sign.add_path \"foobar\"
|-> (fn t => Thm.add_def false false
(Binding.name \"bar_def\", Logic.mk_equals (t, @{term \"%x. x\"})))
@@ -401,8 +401,8 @@
\smallskip\begin{mldecls}
@{ML "thy
-|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
-||>> Sign.declare_const [] ((Binding.name \"foobar\", @{typ \"foo => foo\"}), NoSyn)
+|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
+||>> Sign.declare_const ((Binding.name \"foobar\", @{typ \"foo => foo\"}), NoSyn)
|-> (fn (t1, t2) => Thm.add_def false false
(Binding.name \"bar_def\", Logic.mk_equals (t1, t2)))
"}
@@ -447,7 +447,7 @@
val consts = [\"foo\", \"bar\"];
in
thy
- |> fold_map (fn const => Sign.declare_const []
+ |> fold_map (fn const => Sign.declare_const
((Binding.name const, @{typ \"foo => foo\"}), NoSyn)) consts
|>> map (fn t => Logic.mk_equals (t, @{term \"%x. x\"}))
|-> (fn defs => fold_map (fn def =>
@@ -486,11 +486,11 @@
\smallskip\begin{mldecls}
@{ML "thy
|> tap (fn _ => writeln \"now adding constant\")
-|> Sign.declare_const [] ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
+|> Sign.declare_const ((Binding.name \"bar\", @{typ \"foo => foo\"}), NoSyn)
||>> `(fn thy => Sign.declared_const thy
(Sign.full_name thy (Binding.name \"foobar\")))
|-> (fn (t, b) => if b then I
- else Sign.declare_const []
+ else Sign.declare_const
((Binding.name \"foobar\", @{typ \"foo => foo\"}), NoSyn) #> snd)
"}
\end{mldecls}
--- a/doc-src/IsarImplementation/Thy/Prelim.thy Sun Oct 25 21:35:46 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy Mon Oct 26 08:54:20 2009 +0100
@@ -689,19 +689,19 @@
@{index_ML Long_Name.explode: "string -> string list"} \\
\end{mldecls}
\begin{mldecls}
- @{index_ML_type NameSpace.naming} \\
- @{index_ML NameSpace.default_naming: NameSpace.naming} \\
- @{index_ML NameSpace.add_path: "string -> NameSpace.naming -> NameSpace.naming"} \\
- @{index_ML NameSpace.full_name: "NameSpace.naming -> binding -> string"} \\
+ @{index_ML_type Name_Space.naming} \\
+ @{index_ML Name_Space.default_naming: Name_Space.naming} \\
+ @{index_ML Name_Space.add_path: "string -> Name_Space.naming -> Name_Space.naming"} \\
+ @{index_ML Name_Space.full_name: "Name_Space.naming -> binding -> string"} \\
\end{mldecls}
\begin{mldecls}
- @{index_ML_type NameSpace.T} \\
- @{index_ML NameSpace.empty: NameSpace.T} \\
- @{index_ML NameSpace.merge: "NameSpace.T * NameSpace.T -> NameSpace.T"} \\
- @{index_ML NameSpace.declare: "NameSpace.naming -> binding -> NameSpace.T ->
- string * NameSpace.T"} \\
- @{index_ML NameSpace.intern: "NameSpace.T -> string -> string"} \\
- @{index_ML NameSpace.extern: "NameSpace.T -> string -> string"} \\
+ @{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: "bool -> Name_Space.naming -> binding -> Name_Space.T ->
+ string * Name_Space.T"} \\
+ @{index_ML Name_Space.intern: "Name_Space.T -> string -> string"} \\
+ @{index_ML Name_Space.extern: "Name_Space.T -> string -> string"} \\
\end{mldecls}
\begin{description}
@@ -719,41 +719,43 @@
Long_Name.explode}~@{text "name"} convert between the packed string
representation and the explicit list form of qualified names.
- \item @{ML_type NameSpace.naming} represents the abstract concept of
+ \item @{ML_type Name_Space.naming} represents the abstract concept of
a naming policy.
- \item @{ML NameSpace.default_naming} is the default naming policy.
+ \item @{ML Name_Space.default_naming} is the default naming policy.
In a theory context, this is usually augmented by a path prefix
consisting of the theory name.
- \item @{ML NameSpace.add_path}~@{text "path naming"} augments the
+ \item @{ML Name_Space.add_path}~@{text "path naming"} augments the
naming policy by extending its path component.
- \item @{ML NameSpace.full_name}~@{text "naming binding"} turns a
+ \item @{ML Name_Space.full_name}~@{text "naming binding"} turns a
name binding (usually a basic name) into the fully qualified
internal name, according to the given naming policy.
- \item @{ML_type NameSpace.T} represents name spaces.
+ \item @{ML_type Name_Space.T} represents name spaces.
- \item @{ML NameSpace.empty} and @{ML NameSpace.merge}~@{text
+ \item @{ML Name_Space.empty}~@{text "kind"} and @{ML Name_Space.merge}~@{text
"(space\<^isub>1, space\<^isub>2)"} are the canonical operations for
maintaining name spaces according to theory data management
- (\secref{sec:context-data}).
+ (\secref{sec:context-data}); @{text "kind"} is a formal comment
+ to characterize the purpose of a name space.
- \item @{ML NameSpace.declare}~@{text "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 @{ML Name_Space.declare}~@{text "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 @{ML NameSpace.intern}~@{text "space name"} internalizes a
+ \item @{ML Name_Space.intern}~@{text "space name"} internalizes a
(partially qualified) external name.
This operation is mostly for parsing! Note that fully qualified
names stemming from declarations are produced via @{ML
- "NameSpace.full_name"} and @{ML "NameSpace.declare"}
+ "Name_Space.full_name"} and @{ML "Name_Space.declare"}
(or their derivatives for @{ML_type theory} and
@{ML_type Proof.context}).
- \item @{ML NameSpace.extern}~@{text "space name"} externalizes a
+ \item @{ML Name_Space.extern}~@{text "space name"} externalizes a
(fully qualified) internal name.
This operation is mostly for printing! User code should not rely on
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex Sun Oct 25 21:35:46 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex Mon Oct 26 08:54:20 2009 +0100
@@ -325,9 +325,9 @@
\indexdef{}{ML}{fastype\_of}\verb|fastype_of: term -> typ| \\
\indexdef{}{ML}{lambda}\verb|lambda: term -> term -> term| \\
\indexdef{}{ML}{betapply}\verb|betapply: term * term -> term| \\
- \indexdef{}{ML}{Sign.declare\_const}\verb|Sign.declare_const: Properties.T -> (binding * typ) * mixfix ->|\isasep\isanewline%
+ \indexdef{}{ML}{Sign.declare\_const}\verb|Sign.declare_const: (binding * typ) * mixfix ->|\isasep\isanewline%
\verb| theory -> term * theory| \\
- \indexdef{}{ML}{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> Properties.T -> binding * term ->|\isasep\isanewline%
+ \indexdef{}{ML}{Sign.add\_abbrev}\verb|Sign.add_abbrev: string -> binding * term ->|\isasep\isanewline%
\verb| theory -> (term * term) * theory| \\
\indexdef{}{ML}{Sign.const\_typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
\indexdef{}{ML}{Sign.const\_instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\
@@ -365,11 +365,11 @@
\item \verb|betapply|~\isa{{\isacharparenleft}t{\isacharcomma}\ u{\isacharparenright}} produces an application \isa{t\ u}, with topmost \isa{{\isasymbeta}}-conversion if \isa{t} is an
abstraction.
- \item \verb|Sign.declare_const|~\isa{properties\ {\isacharparenleft}{\isacharparenleft}c{\isacharcomma}\ {\isasymsigma}{\isacharparenright}{\isacharcomma}\ mx{\isacharparenright}}
+ \item \verb|Sign.declare_const|~\isa{{\isacharparenleft}{\isacharparenleft}c{\isacharcomma}\ {\isasymsigma}{\isacharparenright}{\isacharcomma}\ mx{\isacharparenright}}
declares a new constant \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} with optional mixfix
syntax.
- \item \verb|Sign.add_abbrev|~\isa{print{\isacharunderscore}mode\ properties\ {\isacharparenleft}c{\isacharcomma}\ t{\isacharparenright}}
+ \item \verb|Sign.add_abbrev|~\isa{print{\isacharunderscore}mode\ {\isacharparenleft}c{\isacharcomma}\ t{\isacharparenright}}
introduces a new term abbreviation \isa{c\ {\isasymequiv}\ t}.
\item \verb|Sign.const_typargs|~\isa{thy\ {\isacharparenleft}c{\isacharcomma}\ {\isasymtau}{\isacharparenright}} and \verb|Sign.const_instance|~\isa{thy\ {\isacharparenleft}c{\isacharcomma}\ {\isacharbrackleft}{\isasymtau}\isactrlisub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ {\isasymtau}\isactrlisub n{\isacharbrackright}{\isacharparenright}}
--- a/doc-src/IsarImplementation/Thy/document/ML.tex Sun Oct 25 21:35:46 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Mon Oct 26 08:54:20 2009 +0100
@@ -242,14 +242,14 @@
view being presented to the user.
Occasionally, such global process flags are treated like implicit
- arguments to certain operations, by using the \verb|setmp| combinator
+ arguments to certain operations, by using the \verb|setmp_CRITICAL| combinator
for safe temporary assignment. Its traditional purpose was to
ensure proper recovery of the original value when exceptions are
raised in the body, now the functionality is extended to enter the
\emph{critical section} (with its usual potential of degrading
parallelism).
- Note that recovery of plain value passing semantics via \verb|setmp|~\isa{ref\ value} assumes that this \isa{ref} is
+ Note that recovery of plain value passing semantics via \verb|setmp_CRITICAL|~\isa{ref\ value} assumes that this \isa{ref} is
exclusively manipulated within the critical section. In particular,
any persistent global assignment of \isa{ref\ {\isacharcolon}{\isacharequal}\ value} needs to
be marked critical as well, to prevent intruding another threads
@@ -277,7 +277,7 @@
\begin{mldecls}
\indexdef{}{ML}{NAMED\_CRITICAL}\verb|NAMED_CRITICAL: string -> (unit -> 'a) -> 'a| \\
\indexdef{}{ML}{CRITICAL}\verb|CRITICAL: (unit -> 'a) -> 'a| \\
- \indexdef{}{ML}{setmp}\verb|setmp: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c| \\
+ \indexdef{}{ML}{setmp\_CRITICAL}\verb|setmp_CRITICAL: 'a Unsynchronized.ref -> 'a -> ('b -> 'c) -> 'b -> 'c| \\
\end{mldecls}
\begin{description}
@@ -291,7 +291,7 @@
\item \verb|CRITICAL| is the same as \verb|NAMED_CRITICAL| with empty
name argument.
- \item \verb|setmp|~\isa{ref\ value\ f\ x} evaluates \isa{f\ x}
+ \item \verb|setmp_CRITICAL|~\isa{ref\ value\ f\ x} evaluates \isa{f\ x}
while staying within the critical section and having \isa{ref\ {\isacharcolon}{\isacharequal}\ value} assigned temporarily. This recovers a value-passing
semantics involving global references, regardless of exceptions or
concurrency.
@@ -366,7 +366,7 @@
a theory by constant declararion and primitive definitions:
\smallskip\begin{mldecls}
- \verb|Sign.declare_const: Properties.T -> (binding * typ) * mixfix|\isasep\isanewline%
+ \verb|Sign.declare_const: (binding * typ) * mixfix|\isasep\isanewline%
\verb| -> theory -> term * theory| \\
\verb|Thm.add_def: bool -> bool -> binding * term -> theory -> thm * theory|
\end{mldecls}
@@ -378,7 +378,7 @@
\smallskip\begin{mldecls}
\verb|(fn (t, thy) => Thm.add_def false false|\isasep\isanewline%
\verb| (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})) thy)|\isasep\isanewline%
-\verb| (Sign.declare_const []|\isasep\isanewline%
+\verb| (Sign.declare_const|\isasep\isanewline%
\verb| ((Binding.name "bar", @{typ "foo => foo"}), NoSyn) thy)|
\end{mldecls}
@@ -394,7 +394,7 @@
\smallskip\begin{mldecls}
\verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
\verb||\verb,|,\verb|> (fn (t, thy) => thy|\isasep\isanewline%
\verb||\verb,|,\verb|> Thm.add_def false false|\isasep\isanewline%
\verb| (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})))|
@@ -433,7 +433,7 @@
\smallskip\begin{mldecls}
\verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
\verb||\verb,|,\verb|-> (fn t => Thm.add_def false false|\isasep\isanewline%
\verb| (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
@@ -443,7 +443,7 @@
\smallskip\begin{mldecls}
\verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
\verb||\verb,|,\verb|>> (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline%
\verb||\verb,|,\verb|-> (fn def => Thm.add_def false false (Binding.name "bar_def", def))|\isasep\isanewline%
@@ -454,7 +454,7 @@
\smallskip\begin{mldecls}
\verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
\verb||\verb,|,\verb||\verb,|,\verb|> Sign.add_path "foobar"|\isasep\isanewline%
\verb||\verb,|,\verb|-> (fn t => Thm.add_def false false|\isasep\isanewline%
\verb| (Binding.name "bar_def", Logic.mk_equals (t, @{term "%x. x"})))|\isasep\isanewline%
@@ -466,8 +466,8 @@
\smallskip\begin{mldecls}
\verb|thy|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
-\verb||\verb,|,\verb||\verb,|,\verb|>> Sign.declare_const [] ((Binding.name "foobar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb||\verb,|,\verb|>> Sign.declare_const ((Binding.name "foobar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
\verb||\verb,|,\verb|-> (fn (t1, t2) => Thm.add_def false false|\isasep\isanewline%
\verb| (Binding.name "bar_def", Logic.mk_equals (t1, t2)))|\isasep\isanewline%
@@ -527,7 +527,7 @@
\verb| val consts = ["foo", "bar"];|\isasep\isanewline%
\verb|in|\isasep\isanewline%
\verb| thy|\isasep\isanewline%
-\verb| |\verb,|,\verb|> fold_map (fn const => Sign.declare_const []|\isasep\isanewline%
+\verb| |\verb,|,\verb|> fold_map (fn const => Sign.declare_const|\isasep\isanewline%
\verb| ((Binding.name const, @{typ "foo => foo"}), NoSyn)) consts|\isasep\isanewline%
\verb| |\verb,|,\verb|>> map (fn t => Logic.mk_equals (t, @{term "%x. x"}))|\isasep\isanewline%
\verb| |\verb,|,\verb|-> (fn defs => fold_map (fn def =>|\isasep\isanewline%
@@ -596,11 +596,11 @@
\smallskip\begin{mldecls}
\verb|thy|\isasep\isanewline%
\verb||\verb,|,\verb|> tap (fn _ => writeln "now adding constant")|\isasep\isanewline%
-\verb||\verb,|,\verb|> Sign.declare_const [] ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
+\verb||\verb,|,\verb|> Sign.declare_const ((Binding.name "bar", @{typ "foo => foo"}), NoSyn)|\isasep\isanewline%
\verb||\verb,|,\verb||\verb,|,\verb|>> `(fn thy => Sign.declared_const thy|\isasep\isanewline%
\verb| (Sign.full_name thy (Binding.name "foobar")))|\isasep\isanewline%
\verb||\verb,|,\verb|-> (fn (t, b) => if b then I|\isasep\isanewline%
-\verb| else Sign.declare_const []|\isasep\isanewline%
+\verb| else Sign.declare_const|\isasep\isanewline%
\verb| ((Binding.name "foobar", @{typ "foo => foo"}), NoSyn) #> snd)|\isasep\isanewline%
\end{mldecls}%
--- a/doc-src/IsarImplementation/Thy/document/Prelim.tex Sun Oct 25 21:35:46 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Prelim.tex Mon Oct 26 08:54:20 2009 +0100
@@ -798,19 +798,19 @@
\indexdef{}{ML}{Long\_Name.explode}\verb|Long_Name.explode: string -> string list| \\
\end{mldecls}
\begin{mldecls}
- \indexdef{}{ML type}{NameSpace.naming}\verb|type NameSpace.naming| \\
- \indexdef{}{ML}{NameSpace.default\_naming}\verb|NameSpace.default_naming: NameSpace.naming| \\
- \indexdef{}{ML}{NameSpace.add\_path}\verb|NameSpace.add_path: string -> NameSpace.naming -> NameSpace.naming| \\
- \indexdef{}{ML}{NameSpace.full\_name}\verb|NameSpace.full_name: NameSpace.naming -> binding -> string| \\
+ \indexdef{}{ML type}{Name\_Space.naming}\verb|type Name_Space.naming| \\
+ \indexdef{}{ML}{Name\_Space.default\_naming}\verb|Name_Space.default_naming: Name_Space.naming| \\
+ \indexdef{}{ML}{Name\_Space.add\_path}\verb|Name_Space.add_path: string -> Name_Space.naming -> Name_Space.naming| \\
+ \indexdef{}{ML}{Name\_Space.full\_name}\verb|Name_Space.full_name: Name_Space.naming -> binding -> string| \\
\end{mldecls}
\begin{mldecls}
- \indexdef{}{ML type}{NameSpace.T}\verb|type NameSpace.T| \\
- \indexdef{}{ML}{NameSpace.empty}\verb|NameSpace.empty: NameSpace.T| \\
- \indexdef{}{ML}{NameSpace.merge}\verb|NameSpace.merge: NameSpace.T * NameSpace.T -> NameSpace.T| \\
- \indexdef{}{ML}{NameSpace.declare}\verb|NameSpace.declare: NameSpace.naming -> binding -> NameSpace.T ->|\isasep\isanewline%
-\verb| string * NameSpace.T| \\
- \indexdef{}{ML}{NameSpace.intern}\verb|NameSpace.intern: NameSpace.T -> string -> string| \\
- \indexdef{}{ML}{NameSpace.extern}\verb|NameSpace.extern: NameSpace.T -> string -> string| \\
+ \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: bool -> Name_Space.naming -> binding -> Name_Space.T ->|\isasep\isanewline%
+\verb| 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: Name_Space.T -> string -> string| \\
\end{mldecls}
\begin{description}
@@ -827,39 +827,40 @@
\item \verb|Long_Name.implode|~\isa{names} and \verb|Long_Name.explode|~\isa{name} convert between the packed string
representation and the explicit list form of qualified names.
- \item \verb|NameSpace.naming| represents the abstract concept of
+ \item \verb|Name_Space.naming| represents the abstract concept of
a naming policy.
- \item \verb|NameSpace.default_naming| is the default naming policy.
+ \item \verb|Name_Space.default_naming| is the default naming policy.
In a theory context, this is usually augmented by a path prefix
consisting of the theory name.
- \item \verb|NameSpace.add_path|~\isa{path\ naming} augments the
+ \item \verb|Name_Space.add_path|~\isa{path\ naming} augments the
naming policy by extending its path component.
- \item \verb|NameSpace.full_name|~\isa{naming\ binding} turns a
+ \item \verb|Name_Space.full_name|~\isa{naming\ binding} turns a
name binding (usually a basic name) into the fully qualified
internal name, according to the given naming policy.
- \item \verb|NameSpace.T| represents name spaces.
-
- \item \verb|NameSpace.empty| and \verb|NameSpace.merge|~\isa{{\isacharparenleft}space\isactrlisub {\isadigit{1}}{\isacharcomma}\ space\isactrlisub {\isadigit{2}}{\isacharparenright}} are the canonical operations for
- maintaining name spaces according to theory data management
- (\secref{sec:context-data}).
+ \item \verb|Name_Space.T| represents name spaces.
- \item \verb|NameSpace.declare|~\isa{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.empty|~\isa{kind} and \verb|Name_Space.merge|~\isa{{\isacharparenleft}space\isactrlisub {\isadigit{1}}{\isacharcomma}\ space\isactrlisub {\isadigit{2}}{\isacharparenright}} are the canonical operations for
+ maintaining name spaces according to theory data management
+ (\secref{sec:context-data}); \isa{kind} is a formal comment
+ to characterize the purpose of a name space.
- \item \verb|NameSpace.intern|~\isa{space\ name} internalizes a
+ \item \verb|Name_Space.declare|~\isa{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.intern|~\isa{space\ name} internalizes a
(partially qualified) external name.
This operation is mostly for parsing! Note that fully qualified
- names stemming from declarations are produced via \verb|NameSpace.full_name| and \verb|NameSpace.declare|
+ names stemming from declarations are produced via \verb|Name_Space.full_name| and \verb|Name_Space.declare|
(or their derivatives for \verb|theory| and
\verb|Proof.context|).
- \item \verb|NameSpace.extern|~\isa{space\ name} externalizes a
+ \item \verb|Name_Space.extern|~\isa{space\ name} externalizes a
(fully qualified) internal name.
This operation is mostly for printing! User code should not rely on