src/HOL/Tools/Qelim/presburger.ML
changeset 23488 342029af73d1
parent 23469 3f309f885d0b
child 23499 7e27947d92d7
equal deleted inserted replaced
23487:c48defc2b28c 23488:342029af73d1
   146 
   146 
   147 fun eta_beta_tac ctxt i st = case try (nth (cprems_of st)) (i - 1) of
   147 fun eta_beta_tac ctxt i st = case try (nth (cprems_of st)) (i - 1) of
   148    NONE => no_tac st
   148    NONE => no_tac st
   149  | SOME p => 
   149  | SOME p => 
   150    let
   150    let
   151     val eq = (eta_conv (ProofContext.theory_of ctxt) then_conv Thm.beta_conversion true) p
   151     val eq = (Thm.eta_long_conversion then_conv Thm.beta_conversion true) p
   152     val p' = Thm.rhs_of eq
   152     val p' = Thm.rhs_of eq
   153     val th = implies_intr p' (equal_elim (symmetric eq) (assume p'))
   153     val th = implies_intr p' (equal_elim (symmetric eq) (assume p'))
   154    in rtac th i st
   154    in rtac th i st
   155    end;
   155    end;
   156 
   156