summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

NEWS

changeset 73009 | 56eae6d161db |

parent 73008 | dacf2598bb27 |

child 73047 | ab9e27da0e85 |

child 73050 | d77bb4441250 |

equal
deleted
inserted
replaced

73008:dacf2598bb27 | 73009:56eae6d161db |
---|---|

167 |
167 |

168 * Theory "Word": Type word is restricted to bit strings consisting of at |
168 * Theory "Word": Type word is restricted to bit strings consisting of at |

169 least one bit. INCOMPATIBILITY. |
169 least one bit. INCOMPATIBILITY. |

170 |
170 |

171 * Theory "Word": Bit operations NOT, AND, OR, XOR are based on generic |
171 * Theory "Word": Bit operations NOT, AND, OR, XOR are based on generic |

172 algebraic bit operations from HOL-Library.Bit_Operations. |
172 algebraic bit operations from theory "HOL-Library.Bit_Operations". |

173 INCOMPATIBILITY. |
173 INCOMPATIBILITY. |

174 |
174 |

175 * Theory "Word": Most operations on type word are set up for transfer |
175 * Theory "Word": Most operations on type word are set up for transfer |

176 and lifting. INCOMPATIBILITY. |
176 and lifting. INCOMPATIBILITY. |

177 |
177 |