equal
deleted
inserted
replaced
133 relators, and their selectors are now produced using the new BNF-based datatype |
133 relators, and their selectors are now produced using the new BNF-based datatype |
134 package. |
134 package. |
135 Renamed constants: |
135 Renamed constants: |
136 Option.set ~> set_option |
136 Option.set ~> set_option |
137 Option.map ~> map_option |
137 Option.map ~> map_option |
|
138 option_rel ~> rel_option |
138 Renamed theorems: |
139 Renamed theorems: |
139 map_def ~> map_rec[abs_def] |
140 map_def ~> map_rec[abs_def] |
140 Option.map_def ~> map_option_case[abs_def] (with "case_option" instead of "rec_option") |
141 Option.map_def ~> map_option_case[abs_def] (with "case_option" instead of "rec_option") |
141 list_all2_def ~> list_all2_iff |
142 list_all2_def ~> list_all2_iff |
142 map.simps ~> list.map |
143 map.simps ~> list.map |