equal
deleted
inserted
replaced
334 Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_eqvt |
334 Conv.fconv_rule (ih_conv (K (case_hyp RS eq_reflection))) ih_eqvt |
335 |
335 |
336 fun prep_eqvt (RCInfo {llRI, RIvs, CCas, ...}) = |
336 fun prep_eqvt (RCInfo {llRI, RIvs, CCas, ...}) = |
337 (llRI RS ih_eqvt_case) |
337 (llRI RS ih_eqvt_case) |
338 |> fold_rev (Thm.implies_intr o cprop_of) CCas |
338 |> fold_rev (Thm.implies_intr o cprop_of) CCas |
339 |> fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs |
339 (* fold_rev (Thm.forall_intr o cterm_of thy o Free) RIvs *) |
340 in |
340 in |
341 map prep_eqvt RCs |
341 map prep_eqvt RCs |
342 |> map (fold_rev (Thm.implies_intr o cprop_of) ags) |
342 |> map (fold_rev (Thm.implies_intr o cprop_of) ags) |
343 |> map (Thm.implies_intr (cprop_of case_hyp)) |
343 |> map (Thm.implies_intr (cprop_of case_hyp)) |
344 |> map (fold_rev Thm.forall_intr cqs) |
344 |> map (fold_rev Thm.forall_intr cqs) |