removed obsolete eta_long_tac;
authorwenzelm
Tue, 03 Jul 2007 17:17:13 +0200
changeset 23539 df5440e241a1
parent 23538 438e5c4ef2c0
child 23540 77886dfbfa33
removed obsolete eta_long_tac;
src/Pure/tactic.ML
--- a/src/Pure/tactic.ML	Tue Jul 03 17:17:13 2007 +0200
+++ b/src/Pure/tactic.ML	Tue Jul 03 17:17:13 2007 +0200
@@ -75,7 +75,6 @@
   val rotate_tac: int -> int -> tactic
   val defer_tac: int -> tactic
   val filter_prems_tac: (term -> bool) -> int -> tactic
-  val eta_long_tac: int -> tactic
 end;
 
 signature TACTIC =
@@ -560,10 +559,6 @@
        end)
   end;
 
-(*eta long beta normal form*)
-fun eta_long_tac i =
-  PRIMITIVE (Conv.fconv_rule (Conv.goals_conv (fn j => i = j) Thm.eta_long_conversion));
-
 end;
 
 structure BasicTactic: BASIC_TACTIC = Tactic;