equal
deleted
inserted
replaced
175 \indexdef{}{ML}{Variable.declare\_constraints}\verb|Variable.declare_constraints: term -> Proof.context -> Proof.context| \\ |
175 \indexdef{}{ML}{Variable.declare\_constraints}\verb|Variable.declare_constraints: term -> Proof.context -> Proof.context| \\ |
176 \indexdef{}{ML}{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\ |
176 \indexdef{}{ML}{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\ |
177 \indexdef{}{ML}{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\ |
177 \indexdef{}{ML}{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\ |
178 \indexdef{}{ML}{Variable.import}\verb|Variable.import: bool -> thm list -> Proof.context ->|\isasep\isanewline% |
178 \indexdef{}{ML}{Variable.import}\verb|Variable.import: bool -> thm list -> Proof.context ->|\isasep\isanewline% |
179 \verb| (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context| \\ |
179 \verb| (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context| \\ |
180 \indexdef{}{ML}{Variable.focus}\verb|Variable.focus: cterm -> Proof.context ->|\isasep\isanewline% |
180 \indexdef{}{ML}{Variable.focus}\verb|Variable.focus: term -> Proof.context ->|\isasep\isanewline% |
181 \verb| ((string * cterm) list * cterm) * Proof.context| \\ |
181 \verb| ((string * (string * typ)) list * term) * Proof.context| \\ |
182 \end{mldecls} |
182 \end{mldecls} |
183 |
183 |
184 \begin{description} |
184 \begin{description} |
185 |
185 |
186 \item \verb|Variable.add_fixes|~\isa{xs\ ctxt} fixes term |
186 \item \verb|Variable.add_fixes|~\isa{xs\ ctxt} fixes term |