equal
deleted
inserted
replaced
499 |
499 |
500 val unique_clauses = |
500 val unique_clauses = |
501 map2 (mk_uniqueness_clause thy globals compat_store eqvtlems invlems clausei) clauses replems |
501 map2 (mk_uniqueness_clause thy globals compat_store eqvtlems invlems clausei) clauses replems |
502 |
502 |
503 fun elim_implies_eta A AB = |
503 fun elim_implies_eta A AB = |
504 Thm.compose_no_flatten true (A, 0) 1 AB |> Seq.list_of |> the_single |
504 Thm.bicompose {flatten = false, match = true, incremented = false} (false, A, 0) 1 AB |
505 |
505 |> Seq.list_of |> the_single |
|
506 |
506 val uniqueness = G_cases |
507 val uniqueness = G_cases |
507 |> Thm.forall_elim (cterm_of thy lhs) |
508 |> Thm.forall_elim (cterm_of thy lhs) |
508 |> Thm.forall_elim (cterm_of thy y) |
509 |> Thm.forall_elim (cterm_of thy y) |
509 |> Thm.forall_elim P |
510 |> Thm.forall_elim P |
510 |> Thm.elim_implies G_lhs_y |
511 |> Thm.elim_implies G_lhs_y |