equal
deleted
inserted
replaced
55 vacuous propositions of the form SORT_CONSTRAIN('a::c). For example: |
55 vacuous propositions of the form SORT_CONSTRAIN('a::c). For example: |
56 |
56 |
57 lemma assumes "SORT_CONSTRAINT('a::empty)" shows False ... |
57 lemma assumes "SORT_CONSTRAINT('a::empty)" shows False ... |
58 |
58 |
59 The result contains an implicit sort hypotheses as before -- |
59 The result contains an implicit sort hypotheses as before -- |
60 SORT_CONSTRAINT premises are is eliminated as part of the canonical |
60 SORT_CONSTRAINT premises are eliminated as part of the canonical rule |
61 rule normalization. |
61 normalization. |
62 |
62 |
63 * Changed defaults for unify configuration options: |
63 * Changed defaults for unify configuration options: |
64 |
64 |
65 unify_trace_bound = 50 (formerly 25) |
65 unify_trace_bound = 50 (formerly 25) |
66 unify_search_bound = 60 (formerly 30) |
66 unify_search_bound = 60 (formerly 30) |