changeset 4713 | bea2ab2e360b |
parent 4693 | 2e47ea2c6109 |
child 5263 | 8862ed2db431 |
1.1 --- a/src/Pure/tactic.ML Tue Mar 10 13:23:35 1998 +0100 1.2 +++ b/src/Pure/tactic.ML Tue Mar 10 13:24:11 1998 +0100 1.3 @@ -10,7 +10,7 @@ 1.4 sig 1.5 val ares_tac : thm list -> int -> tactic 1.6 val asm_rewrite_goal_tac: 1.7 - bool*bool -> (meta_simpset -> tactic) -> meta_simpset -> int -> tactic 1.8 + bool*bool*bool -> (meta_simpset -> tactic) -> meta_simpset -> int -> tactic 1.9 val assume_tac : int -> tactic 1.10 val atac : int ->tactic 1.11 val bimatch_from_nets_tac: