393 \<close> |
393 \<close> |
394 |
394 |
395 text %mlref \<open> |
395 text %mlref \<open> |
396 \begin{mldecls} |
396 \begin{mldecls} |
397 @{index_ML Rule_Insts.res_inst_tac: "Proof.context -> |
397 @{index_ML Rule_Insts.res_inst_tac: "Proof.context -> |
398 ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\ |
398 ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> |
|
399 thm -> int -> tactic"} \\ |
399 @{index_ML Rule_Insts.eres_inst_tac: "Proof.context -> |
400 @{index_ML Rule_Insts.eres_inst_tac: "Proof.context -> |
400 ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\ |
401 ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> |
|
402 thm -> int -> tactic"} \\ |
401 @{index_ML Rule_Insts.dres_inst_tac: "Proof.context -> |
403 @{index_ML Rule_Insts.dres_inst_tac: "Proof.context -> |
402 ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\ |
404 ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> |
|
405 thm -> int -> tactic"} \\ |
403 @{index_ML Rule_Insts.forw_inst_tac: "Proof.context -> |
406 @{index_ML Rule_Insts.forw_inst_tac: "Proof.context -> |
404 ((indexname * Position.T) * string) list -> thm -> int -> tactic"} \\ |
407 ((indexname * Position.T) * string) list -> (binding * string option * mixfix) list -> |
405 @{index_ML Rule_Insts.subgoal_tac: "Proof.context -> string -> int -> tactic"} \\ |
408 thm -> int -> tactic"} \\ |
406 @{index_ML Rule_Insts.thin_tac: "Proof.context -> string -> int -> tactic"} \\ |
409 @{index_ML Rule_Insts.subgoal_tac: "Proof.context -> string -> |
|
410 (binding * string option * mixfix) list -> int -> tactic"} \\ |
|
411 @{index_ML Rule_Insts.thin_tac: "Proof.context -> string -> |
|
412 (binding * string option * mixfix) list -> int -> tactic"} \\ |
407 @{index_ML rename_tac: "string list -> int -> tactic"} \\ |
413 @{index_ML rename_tac: "string list -> int -> tactic"} \\ |
408 \end{mldecls} |
414 \end{mldecls} |
409 |
415 |
410 \begin{description} |
416 \begin{description} |
411 |
417 |