src/Doc/Implementation/Tactic.thy
changeset 58957 c9e744ea8a38
parent 58956 a816aa3ff391
child 58963 26bf09b95dda
     1.1 --- a/src/Doc/Implementation/Tactic.thy	Sun Nov 09 14:08:00 2014 +0100
     1.2 +++ b/src/Doc/Implementation/Tactic.thy	Sun Nov 09 17:04:14 2014 +0100
     1.3 @@ -284,10 +284,10 @@
     1.4    @{index_ML biresolve_tac: "(bool * thm) list -> int -> tactic"} \\[1ex]
     1.5    @{index_ML assume_tac: "int -> tactic"} \\
     1.6    @{index_ML eq_assume_tac: "int -> tactic"} \\[1ex]
     1.7 -  @{index_ML match_tac: "thm list -> int -> tactic"} \\
     1.8 -  @{index_ML ematch_tac: "thm list -> int -> tactic"} \\
     1.9 -  @{index_ML dmatch_tac: "thm list -> int -> tactic"} \\
    1.10 -  @{index_ML bimatch_tac: "(bool * thm) list -> int -> tactic"} \\
    1.11 +  @{index_ML match_tac: "Proof.context -> thm list -> int -> tactic"} \\
    1.12 +  @{index_ML ematch_tac: "Proof.context -> thm list -> int -> tactic"} \\
    1.13 +  @{index_ML dmatch_tac: "Proof.context -> thm list -> int -> tactic"} \\
    1.14 +  @{index_ML bimatch_tac: "Proof.context -> (bool * thm) list -> int -> tactic"} \\
    1.15    \end{mldecls}
    1.16  
    1.17    \begin{description}