author | wenzelm |
Wed, 12 Jul 2006 21:19:19 +0200 | |
changeset 20115 | 6c2ca3749a80 |
parent 20114 | a1bb4bc68ff3 |
child 20116 | f2aecd6e58ec |
--- a/src/Pure/tactic.ML Wed Jul 12 21:19:17 2006 +0200 +++ b/src/Pure/tactic.ML Wed Jul 12 21:19:19 2006 +0200 @@ -119,6 +119,7 @@ val eres_inst_tac' : (indexname * string) list -> thm -> int -> tactic val res_inst_tac' : (indexname * string) list -> thm -> int -> tactic val instantiate_tac' : (indexname * string) list -> tactic + val make_elim_preserve: thm -> thm end; structure Tactic: TACTIC =