--- a/doc-src/IsarImplementation/Thy/Logic.thy Mon Mar 22 23:34:23 2010 -0700
+++ b/doc-src/IsarImplementation/Thy/Logic.thy Tue Mar 23 12:29:41 2010 +0100
@@ -552,14 +552,13 @@
@{index_ML Thm.implies_elim: "thm -> thm -> thm"} \\
@{index_ML Thm.generalize: "string list * string list -> int -> thm -> thm"} \\
@{index_ML Thm.instantiate: "(ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm"} \\
- @{index_ML Thm.axiom: "theory -> string -> thm"} \\
+ @{index_ML Thm.add_axiom: "binding * term -> theory -> thm * theory"} \\
@{index_ML Thm.add_oracle: "binding * ('a -> cterm) -> theory
-> (string * ('a -> thm)) * theory"} \\
+ @{index_ML Thm.add_def: "bool -> bool -> binding * term -> theory -> thm * theory"} \\
\end{mldecls}
\begin{mldecls}
- @{index_ML Theory.add_axioms_i: "(binding * term) list -> theory -> theory"} \\
@{index_ML Theory.add_deps: "string -> string * typ -> (string * typ) list -> theory -> theory"} \\
- @{index_ML Theory.add_defs_i: "bool -> bool -> (binding * term) list -> theory -> theory"} \\
\end{mldecls}
\begin{description}
@@ -607,26 +606,28 @@
term variables. Note that the types in @{text "\<^vec>x\<^isub>\<tau>"}
refer to the instantiated versions.
- \item @{ML Thm.axiom}~@{text "thy name"} retrieves a named
- axiom, cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
+ \item @{ML Thm.add_axiom}~@{text "(name, A) thy"} declares an
+ arbitrary proposition as axiom, and retrieves it as a theorem from
+ the resulting theory, cf.\ @{text "axiom"} in
+ \figref{fig:prim-rules}. Note that the low-level representation in
+ the axiom table may differ slightly from the returned theorem.
\item @{ML Thm.add_oracle}~@{text "(binding, oracle)"} produces a named
oracle rule, essentially generating arbitrary axioms on the fly,
cf.\ @{text "axiom"} in \figref{fig:prim-rules}.
- \item @{ML Theory.add_axioms_i}~@{text "[(name, A), \<dots>]"} declares
- arbitrary propositions as axioms.
+ \item @{ML Thm.add_def}~@{text "unchecked overloaded (name, c
+ \<^vec>x \<equiv> t)"} states a definitional axiom for an existing constant
+ @{text "c"}. Dependencies are recorded via @{ML Theory.add_deps},
+ unless the @{text "unchecked"} option is set. Note that the
+ low-level representation in the axiom table may differ slightly from
+ the returned theorem.
\item @{ML Theory.add_deps}~@{text "name c\<^isub>\<tau>
\<^vec>d\<^isub>\<sigma>"} declares dependencies of a named specification
for constant @{text "c\<^isub>\<tau>"}, relative to existing
specifications for constants @{text "\<^vec>d\<^isub>\<sigma>"}.
- \item @{ML Theory.add_defs_i}~@{text "unchecked overloaded [(name, c
- \<^vec>x \<equiv> t), \<dots>]"} states a definitional axiom for an existing
- constant @{text "c"}. Dependencies are recorded (cf.\ @{ML
- Theory.add_deps}), unless the @{text "unchecked"} option is set.
-
\end{description}
*}
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex Mon Mar 22 23:34:23 2010 -0700
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex Tue Mar 23 12:29:41 2010 +0100
@@ -560,14 +560,13 @@
\indexdef{}{ML}{Thm.implies\_elim}\verb|Thm.implies_elim: thm -> thm -> thm| \\
\indexdef{}{ML}{Thm.generalize}\verb|Thm.generalize: string list * string list -> int -> thm -> thm| \\
\indexdef{}{ML}{Thm.instantiate}\verb|Thm.instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm| \\
- \indexdef{}{ML}{Thm.axiom}\verb|Thm.axiom: theory -> string -> thm| \\
+ \indexdef{}{ML}{Thm.add\_axiom}\verb|Thm.add_axiom: binding * term -> theory -> thm * theory| \\
\indexdef{}{ML}{Thm.add\_oracle}\verb|Thm.add_oracle: binding * ('a -> cterm) -> theory|\isasep\isanewline%
\verb| -> (string * ('a -> thm)) * theory| \\
+ \indexdef{}{ML}{Thm.add\_def}\verb|Thm.add_def: bool -> bool -> binding * term -> theory -> thm * theory| \\
\end{mldecls}
\begin{mldecls}
- \indexdef{}{ML}{Theory.add\_axioms\_i}\verb|Theory.add_axioms_i: (binding * term) list -> theory -> theory| \\
\indexdef{}{ML}{Theory.add\_deps}\verb|Theory.add_deps: string -> string * typ -> (string * typ) list -> theory -> theory| \\
- \indexdef{}{ML}{Theory.add\_defs\_i}\verb|Theory.add_defs_i: bool -> bool -> (binding * term) list -> theory -> theory| \\
\end{mldecls}
\begin{description}
@@ -612,23 +611,26 @@
term variables. Note that the types in \isa{\isactrlvec x\isactrlisub {\isasymtau}}
refer to the instantiated versions.
- \item \verb|Thm.axiom|~\isa{thy\ name} retrieves a named
- axiom, cf.\ \isa{axiom} in \figref{fig:prim-rules}.
+ \item \verb|Thm.add_axiom|~\isa{{\isacharparenleft}name{\isacharcomma}\ A{\isacharparenright}\ thy} declares an
+ arbitrary proposition as axiom, and retrieves it as a theorem from
+ the resulting theory, cf.\ \isa{axiom} in
+ \figref{fig:prim-rules}. Note that the low-level representation in
+ the axiom table may differ slightly from the returned theorem.
\item \verb|Thm.add_oracle|~\isa{{\isacharparenleft}binding{\isacharcomma}\ oracle{\isacharparenright}} produces a named
oracle rule, essentially generating arbitrary axioms on the fly,
cf.\ \isa{axiom} in \figref{fig:prim-rules}.
- \item \verb|Theory.add_axioms_i|~\isa{{\isacharbrackleft}{\isacharparenleft}name{\isacharcomma}\ A{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares
- arbitrary propositions as axioms.
+ \item \verb|Thm.add_def|~\isa{unchecked\ overloaded\ {\isacharparenleft}name{\isacharcomma}\ c\ \isactrlvec x\ {\isasymequiv}\ t{\isacharparenright}} states a definitional axiom for an existing constant
+ \isa{c}. Dependencies are recorded via \verb|Theory.add_deps|,
+ unless the \isa{unchecked} option is set. Note that the
+ low-level representation in the axiom table may differ slightly from
+ the returned theorem.
\item \verb|Theory.add_deps|~\isa{name\ c\isactrlisub {\isasymtau}\ \isactrlvec d\isactrlisub {\isasymsigma}} declares dependencies of a named specification
for constant \isa{c\isactrlisub {\isasymtau}}, relative to existing
specifications for constants \isa{\isactrlvec d\isactrlisub {\isasymsigma}}.
- \item \verb|Theory.add_defs_i|~\isa{unchecked\ overloaded\ {\isacharbrackleft}{\isacharparenleft}name{\isacharcomma}\ c\ \isactrlvec x\ {\isasymequiv}\ t{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} states a definitional axiom for an existing
- constant \isa{c}. Dependencies are recorded (cf.\ \verb|Theory.add_deps|), unless the \isa{unchecked} option is set.
-
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%