equal
deleted
inserted
replaced
50 lemma "P (x::'a)" and "Q (y::'a::bar)" |
50 lemma "P (x::'a)" and "Q (y::'a::bar)" |
51 -- "now uniform 'a::bar instead of default sort for first occurence (!)" |
51 -- "now uniform 'a::bar instead of default sort for first occurence (!)" |
52 |
52 |
53 |
53 |
54 *** HOL *** |
54 *** HOL *** |
|
55 |
|
56 * 'datatype' specifications allow explicit sort constraints. |
55 |
57 |
56 * Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY, use |
58 * Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY, use |
57 theory HOL/Library/Nat_Bijection instead. |
59 theory HOL/Library/Nat_Bijection instead. |
58 |
60 |
59 * Session HOL-Word: Discontinued many redundant theorems specific to type |
61 * Session HOL-Word: Discontinued many redundant theorems specific to type |