equal
deleted
inserted
replaced
392 instantiations are seldom necessary. |
392 instantiations are seldom necessary. |
393 \<close> |
393 \<close> |
394 |
394 |
395 text %mlref \<open> |
395 text %mlref \<open> |
396 \begin{mldecls} |
396 \begin{mldecls} |
397 @{index_ML res_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\ |
397 @{index_ML res_inst_tac: "Proof.context -> |
398 @{index_ML eres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\ |
398 ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\ |
399 @{index_ML dres_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\ |
399 @{index_ML eres_inst_tac: "Proof.context -> |
400 @{index_ML forw_inst_tac: "Proof.context -> (indexname * string) list -> thm -> int -> tactic"} \\ |
400 ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\ |
|
401 @{index_ML dres_inst_tac: "Proof.context -> |
|
402 ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\ |
|
403 @{index_ML forw_inst_tac: "Proof.context -> |
|
404 ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\ |
401 @{index_ML subgoal_tac: "Proof.context -> string -> int -> tactic"} \\ |
405 @{index_ML subgoal_tac: "Proof.context -> string -> int -> tactic"} \\ |
402 @{index_ML thin_tac: "Proof.context -> string -> int -> tactic"} \\ |
406 @{index_ML thin_tac: "Proof.context -> string -> int -> tactic"} \\ |
403 @{index_ML rename_tac: "string list -> int -> tactic"} \\ |
407 @{index_ML rename_tac: "string list -> int -> tactic"} \\ |
404 \end{mldecls} |
408 \end{mldecls} |
405 |
409 |