src/Pure/tactic.ML
changeset 23492 60cf5cf30b81
parent 23223 7791128b39a9
child 23539 df5440e241a1
     1.1 --- a/src/Pure/tactic.ML	Mon Jun 25 00:36:40 2007 +0200
     1.2 +++ b/src/Pure/tactic.ML	Mon Jun 25 00:36:41 2007 +0200
     1.3 @@ -75,6 +75,7 @@
     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 @@ -559,6 +560,10 @@
    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;