Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
generate theorems like 'bool.split_sel'
authorblanchet
Fri, 11 Mar 2016 08:39:57 +0100
changeset 62594 75452e3eda14
parent 62593 adffc55a682d
child 62595 092c63734cc6
generate theorems like 'bool.split_sel'
src/HOL/Product_Type.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Product_Type.thy	Thu Mar 10 22:49:24 2016 +0100
+++ b/src/HOL/Product_Type.thy	Fri Mar 11 08:39:57 2016 +0100
@@ -12,7 +12,7 @@
 
 subsection \<open>@{typ bool} is a datatype\<close>
 
-free_constructors case_bool for True | False
+free_constructors (discs_sels) case_bool for True | False
   by auto
 
 text \<open>Avoid name clashes by prefixing the output of \<open>old_rep_datatype\<close> with \<open>old\<close>.\<close>
isabelle