| author | wenzelm |
| Sun, 14 Oct 2001 20:08:42 +0200 | |
| changeset 11762 | 7aa0702d3340 |
| parent 10212 | 33fe2d701ddd |
| child 11954 | 3d1780208bf3 |
| permissions | -rw-r--r-- |
(* Title: HOL/Datatype.thy ID: $Id$ Author: Stefan Berghofer Copyright 1998 TU Muenchen *) Datatype = Datatype_Universe + rep_datatype bool distinct True_not_False, False_not_True induct bool_induct rep_datatype sum distinct Inl_not_Inr, Inr_not_Inl inject Inl_eq, Inr_eq induct sum_induct rep_datatype prod inject Pair_eq induct prod_induct rep_datatype unit induct unit_induct end