summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | haftmann |

Sat, 25 Sep 2021 07:45:27 +0000 | |

changeset 74364 | 99add5178e51 |

parent 74363 | 383fd113baae |

child 74366 | d1185d02aef5 |

NOT is part of syntax bundle also

NEWS | file | annotate | diff | comparison | revisions | |

src/HOL/Bit_Operations.thy | file | annotate | diff | comparison | revisions |

--- a/NEWS Fri Sep 24 22:44:13 2021 +0200 +++ b/NEWS Sat Sep 25 07:45:27 2021 +0000 @@ -205,7 +205,7 @@ * Combinator "Fun.swap" resolved into a mere input abbreviation in separate theory "Transposition" in HOL-Combinatorics. INCOMPATIBILITY. -* Infix syntax for bit operations AND, OR, XOR is now organized in +* Infix syntax for bit operations AND, OR, XOR, NOT is now organized in bundle bit_operations_syntax. INCOMPATIBILITY. * Bit operations set_bit, unset_bit and flip_bit are now class

--- a/src/HOL/Bit_Operations.thy Fri Sep 24 22:44:13 2021 +0200 +++ b/src/HOL/Bit_Operations.thy Sat Sep 25 07:45:27 2021 +0000 @@ -3509,7 +3509,8 @@ \<close> no_notation - "and" (infixr \<open>AND\<close> 64) + not (\<open>NOT"\<close>) + and "and" (infixr \<open>AND\<close> 64) and or (infixr \<open>OR\<close> 59) and xor (infixr \<open>XOR\<close> 59) @@ -3517,7 +3518,8 @@ begin notation - "and" (infixr \<open>AND\<close> 64) + not (\<open>NOT"\<close>) + and "and" (infixr \<open>AND\<close> 64) and or (infixr \<open>OR\<close> 59) and xor (infixr \<open>XOR\<close> 59)