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 * Theory HOL/Library/Diagonalize has been removed. INCOMPATIBILITY, use |
|
57 theory HOL/Library/Nat_Bijection instead. |
55 |
58 |
56 * Session HOL-Word: Discontinued many redundant theorems specific to type |
59 * Session HOL-Word: Discontinued many redundant theorems specific to type |
57 'a word. INCOMPATIBILITY, use the corresponding generic theorems instead. |
60 'a word. INCOMPATIBILITY, use the corresponding generic theorems instead. |
58 |
61 |
59 word_sub_alt ~> word_sub_wi |
62 word_sub_alt ~> word_sub_wi |