equal
deleted
inserted
replaced
349 |
349 |
350 val unique_clauses = |
350 val unique_clauses = |
351 map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas |
351 map2 (mk_uniqueness_clause thy globals compat_store clausei) clauses rep_lemmas |
352 |
352 |
353 fun elim_implies_eta A AB = |
353 fun elim_implies_eta A AB = |
354 Thm.bicompose {flatten = false, match = true, incremented = false} (false, A, 0) 1 AB |
354 Thm.bicompose (SOME ctxt) {flatten = false, match = true, incremented = false} |
|
355 (false, A, 0) 1 AB |
355 |> Seq.list_of |> the_single |
356 |> Seq.list_of |> the_single |
356 |
357 |
357 val uniqueness = G_cases |
358 val uniqueness = G_cases |
358 |> Thm.forall_elim (cterm_of thy lhs) |
359 |> Thm.forall_elim (cterm_of thy lhs) |
359 |> Thm.forall_elim (cterm_of thy y) |
360 |> Thm.forall_elim (cterm_of thy y) |