equal
deleted
inserted
replaced
136 INCOMPATIBILITY |
136 INCOMPATIBILITY |
137 - Removed lemmas generated by lift_definition: |
137 - Removed lemmas generated by lift_definition: |
138 less_eq_multiset.abs_eq, less_eq_multiset.rsp less_eq_multiset.transfer |
138 less_eq_multiset.abs_eq, less_eq_multiset.rsp less_eq_multiset.transfer |
139 less_eq_multiset_def |
139 less_eq_multiset_def |
140 INCOMPATIBILITY |
140 INCOMPATIBILITY |
|
141 |
|
142 * Theory Library/Old_Recdef: discontinued obsolete 'defer_recdef' |
|
143 command. Minor INCOMPATIBILITY, use 'function' instead. |
141 |
144 |
142 |
145 |
143 |
146 |
144 New in Isabelle2015 (May 2015) |
147 New in Isabelle2015 (May 2015) |
145 ------------------------------ |
148 ------------------------------ |