removed obsolete eta_long_tac;
authorwenzelm
Tue Jul 03 17:17:13 2007 +0200 (2007-07-03)
changeset 23539df5440e241a1
parent 23538 438e5c4ef2c0
child 23540 77886dfbfa33
removed obsolete eta_long_tac;
src/Pure/tactic.ML
     1.1 --- a/src/Pure/tactic.ML	Tue Jul 03 17:17:13 2007 +0200
     1.2 +++ b/src/Pure/tactic.ML	Tue Jul 03 17:17:13 2007 +0200
     1.3 @@ -75,7 +75,6 @@
     1.4    val rotate_tac: int -> int -> tactic
     1.5    val defer_tac: int -> tactic
     1.6    val filter_prems_tac: (term -> bool) -> int -> tactic
     1.7 -  val eta_long_tac: int -> tactic
     1.8  end;
     1.9  
    1.10  signature TACTIC =
    1.11 @@ -560,10 +559,6 @@
    1.12         end)
    1.13    end;
    1.14  
    1.15 -(*eta long beta normal form*)
    1.16 -fun eta_long_tac i =
    1.17 -  PRIMITIVE (Conv.fconv_rule (Conv.goals_conv (fn j => i = j) Thm.eta_long_conversion));
    1.18 -
    1.19  end;
    1.20  
    1.21  structure BasicTactic: BASIC_TACTIC = Tactic;