updated;
authorwenzelm
Wed Dec 13 16:26:45 2006 +0100 (2006-12-13)
changeset 218270b1d07f79c1e
parent 21826 b90d927e0a4b
child 21828 b8166438c772
updated;
doc-src/IsarImplementation/Thy/document/logic.tex
doc-src/IsarImplementation/Thy/document/proof.tex
doc-src/IsarImplementation/Thy/logic.thy
doc-src/IsarImplementation/Thy/proof.thy
     1.1 --- a/doc-src/IsarImplementation/Thy/document/logic.tex	Wed Dec 13 15:47:37 2006 +0100
     1.2 +++ b/doc-src/IsarImplementation/Thy/document/logic.tex	Wed Dec 13 16:26:45 2006 +0100
     1.3 @@ -329,8 +329,7 @@
     1.4    \indexml{lambda}\verb|lambda: term -> term -> term| \\
     1.5    \indexml{betapply}\verb|betapply: term * term -> term| \\
     1.6    \indexml{Sign.add-consts-i}\verb|Sign.add_consts_i: (string * typ * mixfix) list -> theory -> theory| \\
     1.7 -  \indexml{Sign.add-abbrevs}\verb|Sign.add_abbrevs: string * bool ->|\isasep\isanewline%
     1.8 -\verb|  ((string * mixfix) * term) list -> theory -> (term * term) list * theory| \\
     1.9 +  \indexml{Sign.add-abbrev}\verb|Sign.add_abbrev: string -> bstring * term -> theory -> (term * term) * theory| \\
    1.10    \indexml{Sign.const-typargs}\verb|Sign.const_typargs: theory -> string * typ -> typ list| \\
    1.11    \indexml{Sign.const-instance}\verb|Sign.const_instance: theory -> string * typ list -> typ| \\
    1.12    \end{mldecls}
    1.13 @@ -370,9 +369,8 @@
    1.14    \item \verb|Sign.add_consts_i|~\isa{{\isacharbrackleft}{\isacharparenleft}c{\isacharcomma}\ {\isasymsigma}{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}} declares a
    1.15    new constant \isa{c\ {\isacharcolon}{\isacharcolon}\ {\isasymsigma}} with optional mixfix syntax.
    1.16  
    1.17 -  \item \verb|Sign.add_abbrevs|~\isa{print{\isacharunderscore}mode\ {\isacharbrackleft}{\isacharparenleft}{\isacharparenleft}c{\isacharcomma}\ t{\isacharparenright}{\isacharcomma}\ mx{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}}
    1.18 -  declares a new term abbreviation \isa{c\ {\isasymequiv}\ t} with optional
    1.19 -  mixfix syntax.
    1.20 +  \item \verb|Sign.add_abbrev|~\isa{print{\isacharunderscore}mode\ {\isacharparenleft}c{\isacharcomma}\ t{\isacharparenright}}
    1.21 +  introduces a new term abbreviation \isa{c\ {\isasymequiv}\ t}.
    1.22  
    1.23    \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}}
    1.24    convert between two representations of polymorphic constants: full
     2.1 --- a/doc-src/IsarImplementation/Thy/document/proof.tex	Wed Dec 13 15:47:37 2006 +0100
     2.2 +++ b/doc-src/IsarImplementation/Thy/document/proof.tex	Wed Dec 13 16:26:45 2006 +0100
     2.3 @@ -356,8 +356,8 @@
     2.4  
     2.5    \item \verb|Goal.prove_multi| is simular to \verb|Goal.prove|, but
     2.6    states several conclusions simultaneously.  The goal is encoded by
     2.7 -  means of Pure conjunction; \verb|Tactic.conjunction_tac| will turn
     2.8 -  this into a collection of individual subgoals.
     2.9 +  means of Pure conjunction; \verb|Goal.conjunction_tac| will turn this
    2.10 +  into a collection of individual subgoals.
    2.11  
    2.12    \item \verb|Obtain.result|~\isa{tac\ thms\ ctxt} eliminates the
    2.13    given facts using a tactic, which results in additional fixed
     3.1 --- a/doc-src/IsarImplementation/Thy/logic.thy	Wed Dec 13 15:47:37 2006 +0100
     3.2 +++ b/doc-src/IsarImplementation/Thy/logic.thy	Wed Dec 13 16:26:45 2006 +0100
     3.3 @@ -327,8 +327,7 @@
     3.4    @{index_ML lambda: "term -> term -> term"} \\
     3.5    @{index_ML betapply: "term * term -> term"} \\
     3.6    @{index_ML Sign.add_consts_i: "(string * typ * mixfix) list -> theory -> theory"} \\
     3.7 -  @{index_ML Sign.add_abbrevs: "string * bool ->
     3.8 -  ((string * mixfix) * term) list -> theory -> (term * term) list * theory"} \\
     3.9 +  @{index_ML Sign.add_abbrev: "string -> bstring * term -> theory -> (term * term) * theory"} \\
    3.10    @{index_ML Sign.const_typargs: "theory -> string * typ -> typ list"} \\
    3.11    @{index_ML Sign.const_instance: "theory -> string * typ list -> typ"} \\
    3.12    \end{mldecls}
    3.13 @@ -376,9 +375,8 @@
    3.14    \item @{ML Sign.add_consts_i}~@{text "[(c, \<sigma>, mx), \<dots>]"} declares a
    3.15    new constant @{text "c :: \<sigma>"} with optional mixfix syntax.
    3.16  
    3.17 -  \item @{ML Sign.add_abbrevs}~@{text "print_mode [((c, t), mx), \<dots>]"}
    3.18 -  declares a new term abbreviation @{text "c \<equiv> t"} with optional
    3.19 -  mixfix syntax.
    3.20 +  \item @{ML Sign.add_abbrev}~@{text "print_mode (c, t)"}
    3.21 +  introduces a new term abbreviation @{text "c \<equiv> t"}.
    3.22  
    3.23    \item @{ML Sign.const_typargs}~@{text "thy (c, \<tau>)"} and @{ML
    3.24    Sign.const_instance}~@{text "thy (c, [\<tau>\<^isub>1, \<dots>, \<tau>\<^isub>n])"}
     4.1 --- a/doc-src/IsarImplementation/Thy/proof.thy	Wed Dec 13 15:47:37 2006 +0100
     4.2 +++ b/doc-src/IsarImplementation/Thy/proof.thy	Wed Dec 13 16:26:45 2006 +0100
     4.3 @@ -318,8 +318,8 @@
     4.4  
     4.5    \item @{ML Goal.prove_multi} is simular to @{ML Goal.prove}, but
     4.6    states several conclusions simultaneously.  The goal is encoded by
     4.7 -  means of Pure conjunction; @{ML Tactic.conjunction_tac} will turn
     4.8 -  this into a collection of individual subgoals.
     4.9 +  means of Pure conjunction; @{ML Goal.conjunction_tac} will turn this
    4.10 +  into a collection of individual subgoals.
    4.11  
    4.12    \item @{ML Obtain.result}~@{text "tac thms ctxt"} eliminates the
    4.13    given facts using a tactic, which results in additional fixed