updated Variable.focus;
authorwenzelm
Sat Apr 30 23:27:57 2011 +0200 (2011-04-30)
changeset 425099d107a52b634
parent 42508 e21362bf1d93
child 42510 b9c106763325
updated Variable.focus;
doc-src/IsarImplementation/Thy/Proof.thy
doc-src/IsarImplementation/Thy/document/Proof.tex
     1.1 --- a/doc-src/IsarImplementation/Thy/Proof.thy	Sat Apr 30 23:20:50 2011 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/Proof.thy	Sat Apr 30 23:27:57 2011 +0200
     1.3 @@ -109,8 +109,8 @@
     1.4    @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
     1.5    @{index_ML Variable.import: "bool -> thm list -> Proof.context ->
     1.6    (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context"} \\
     1.7 -  @{index_ML Variable.focus: "cterm -> Proof.context ->
     1.8 -  ((string * cterm) list * cterm) * Proof.context"} \\
     1.9 +  @{index_ML Variable.focus: "term -> Proof.context ->
    1.10 +  ((string * (string * typ)) list * term) * Proof.context"} \\
    1.11    \end{mldecls}
    1.12  
    1.13    \begin{description}
     2.1 --- a/doc-src/IsarImplementation/Thy/document/Proof.tex	Sat Apr 30 23:20:50 2011 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/document/Proof.tex	Sat Apr 30 23:27:57 2011 +0200
     2.3 @@ -177,8 +177,8 @@
     2.4    \indexdef{}{ML}{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\
     2.5    \indexdef{}{ML}{Variable.import}\verb|Variable.import: bool -> thm list -> Proof.context ->|\isasep\isanewline%
     2.6  \verb|  (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context| \\
     2.7 -  \indexdef{}{ML}{Variable.focus}\verb|Variable.focus: cterm -> Proof.context ->|\isasep\isanewline%
     2.8 -\verb|  ((string * cterm) list * cterm) * Proof.context| \\
     2.9 +  \indexdef{}{ML}{Variable.focus}\verb|Variable.focus: term -> Proof.context ->|\isasep\isanewline%
    2.10 +\verb|  ((string * (string * typ)) list * term) * Proof.context| \\
    2.11    \end{mldecls}
    2.12  
    2.13    \begin{description}