# HG changeset patch # User wenzelm # Date 1249151674 -7200 # Node ID aa48c2b8f8e023b5334758bbe885b3ed5dc8f66d # Parent 2b64fbc54a828743576c5cba50394f824bd311fe updated Variable.import; diff -r 2b64fbc54a82 -r aa48c2b8f8e0 doc-src/IsarImplementation/Thy/Proof.thy --- a/doc-src/IsarImplementation/Thy/Proof.thy Sat Aug 01 00:39:51 2009 +0200 +++ b/doc-src/IsarImplementation/Thy/Proof.thy Sat Aug 01 20:34:34 2009 +0200 @@ -94,7 +94,7 @@ @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\ @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\ @{index_ML Variable.import: "bool -> thm list -> Proof.context -> - ((ctyp list * cterm list) * thm list) * Proof.context"} \\ + (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context"} \\ @{index_ML Variable.focus: "cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context"} \\ \end{mldecls} diff -r 2b64fbc54a82 -r aa48c2b8f8e0 doc-src/IsarImplementation/Thy/document/Proof.tex --- a/doc-src/IsarImplementation/Thy/document/Proof.tex Sat Aug 01 00:39:51 2009 +0200 +++ b/doc-src/IsarImplementation/Thy/document/Proof.tex Sat Aug 01 20:34:34 2009 +0200 @@ -112,7 +112,7 @@ \indexdef{}{ML}{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\ \indexdef{}{ML}{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\ \indexdef{}{ML}{Variable.import}\verb|Variable.import: bool -> thm list -> Proof.context ->|\isasep\isanewline% -\verb| ((ctyp list * cterm list) * thm list) * Proof.context| \\ +\verb| (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context| \\ \indexdef{}{ML}{Variable.focus}\verb|Variable.focus: cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context| \\ \end{mldecls}