equal
deleted
inserted
replaced
85 setup {* |
85 setup {* |
86 RType.add_def @{type_name prop} |
86 RType.add_def @{type_name prop} |
87 #> RType.add_def @{type_name fun} |
87 #> RType.add_def @{type_name fun} |
88 #> RType.add_def @{type_name itself} |
88 #> RType.add_def @{type_name itself} |
89 #> RType.add_def @{type_name bool} |
89 #> RType.add_def @{type_name bool} |
90 #> RType.add_def @{type_name set} |
|
91 #> TypedefPackage.interpretation RType.perhaps_add_def |
90 #> TypedefPackage.interpretation RType.perhaps_add_def |
92 *} |
91 *} |
93 |
92 |
94 lemma [code func]: |
93 lemma [code func]: |
95 "RType tyco1 tys1 = RType tyco2 tys2 \<longleftrightarrow> tyco1 = tyco2 |
94 "RType tyco1 tys1 = RType tyco2 tys2 \<longleftrightarrow> tyco1 = tyco2 |