| changeset 68778 | 4566bac4517d |
| parent 67406 | 23307fd33906 |
| child 69505 | cc2d676d5395 |
--- a/src/HOL/IMP/Abs_Int1_parity.thy Mon Aug 20 20:54:40 2018 +0200 +++ b/src/HOL/IMP/Abs_Int1_parity.thy Tue Aug 21 17:29:46 2018 +0200 @@ -1,11 +1,11 @@ (* Author: Tobias Nipkow *) +subsection "Parity Analysis" + theory Abs_Int1_parity imports Abs_Int1 begin -subsection "Parity Analysis" - datatype parity = Even | Odd | Either text\<open>Instantiation of class @{class order} with type @{typ parity}:\<close>