removed Variable.monomorphic;
authorwenzelm
Thu Jul 20 14:35:37 2006 +0200 (2006-07-20)
changeset 20171424739228123
parent 20170 6ff853f82d73
child 20172 b65eb8145f5e
removed Variable.monomorphic;
doc-src/IsarImplementation/Thy/document/proof.tex
doc-src/IsarImplementation/Thy/proof.thy
     1.1 --- a/doc-src/IsarImplementation/Thy/document/proof.tex	Thu Jul 20 14:34:57 2006 +0200
     1.2 +++ b/doc-src/IsarImplementation/Thy/document/proof.tex	Thu Jul 20 14:35:37 2006 +0200
     1.3 @@ -49,7 +49,6 @@
     1.4    \indexml{Variable.import}\verb|Variable.import: bool -> thm list -> Proof.context -> thm list * Proof.context| \\
     1.5    \indexml{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\
     1.6    \indexml{Variable.trade}\verb|Variable.trade: Proof.context -> (thm list -> thm list) -> thm list -> thm list| \\
     1.7 -  \indexml{Variable.monomorphic}\verb|Variable.monomorphic: Proof.context -> term list -> term list| \\
     1.8    \indexml{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\
     1.9    \end{mldecls}
    1.10  
    1.11 @@ -84,9 +83,6 @@
    1.12    \item \verb|Variable.trade| composes \verb|Variable.import| and \verb|Variable.export|, i.e.\ it provides a view on facts with all
    1.13    variables being fixed in the current context.
    1.14  
    1.15 -  \item \verb|Variable.monomorphic|~\isa{ctxt\ ts} introduces fixed
    1.16 -  type variables for the schematic ones in \isa{ts}.
    1.17 -
    1.18    \item \verb|Variable.polymorphic|~\isa{ctxt\ ts} generalizes type
    1.19    variables in \isa{ts} as far as possible, even those occurring
    1.20    in fixed term variables.  This operation essentially reverses the
     2.1 --- a/doc-src/IsarImplementation/Thy/proof.thy	Thu Jul 20 14:34:57 2006 +0200
     2.2 +++ b/doc-src/IsarImplementation/Thy/proof.thy	Thu Jul 20 14:35:37 2006 +0200
     2.3 @@ -18,7 +18,6 @@
     2.4    @{index_ML Variable.import: "bool -> thm list -> Proof.context -> thm list * Proof.context"} \\
     2.5    @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
     2.6    @{index_ML Variable.trade: "Proof.context -> (thm list -> thm list) -> thm list -> thm list"} \\
     2.7 -  @{index_ML Variable.monomorphic: "Proof.context -> term list -> term list"} \\
     2.8    @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
     2.9    \end{mldecls}
    2.10  
    2.11 @@ -56,9 +55,6 @@
    2.12    Variable.export}, i.e.\ it provides a view on facts with all
    2.13    variables being fixed in the current context.
    2.14  
    2.15 -  \item @{ML Variable.monomorphic}~@{text "ctxt ts"} introduces fixed
    2.16 -  type variables for the schematic ones in @{text "ts"}.
    2.17 -
    2.18    \item @{ML Variable.polymorphic}~@{text "ctxt ts"} generalizes type
    2.19    variables in @{text "ts"} as far as possible, even those occurring
    2.20    in fixed term variables.  This operation essentially reverses the