# HG changeset patch # User wenzelm # Date 1152731959 -7200 # Node ID 6c2ca3749a8051a7b70ac86e2e3b8869f5f1fee5 # Parent a1bb4bc68ff3c3d5453aeb5ae5eb45309588418c exported make_elim_preserve; diff -r a1bb4bc68ff3 -r 6c2ca3749a80 src/Pure/tactic.ML --- 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 =