| changeset 57091 | 1fa9c19ba2c9 |
| parent 57016 | c44ce6f4067d |
| child 57201 | 697e0fad9337 |
--- a/src/HOL/Product_Type.thy Mon May 26 16:32:51 2014 +0200 +++ b/src/HOL/Product_Type.thy Mon May 26 16:32:55 2014 +0200 @@ -12,7 +12,7 @@ subsection {* @{typ bool} is a datatype *} -free_constructors case_bool for =: True | False +free_constructors case_bool for True | False by auto text {* Avoid name clashes by prefixing the output of @{text rep_datatype} with @{text old}. *}