| changeset 58976 | b38a54bbfbd6 |
| parent 58971 | 8c9a319821b3 |
| child 58977 | 9576b510f6a2 |
--- a/src/CCL/Type.thy Tue Nov 11 13:44:09 2014 +0100 +++ b/src/CCL/Type.thy Tue Nov 11 13:50:56 2014 +0100 @@ -100,9 +100,7 @@ and TexXH: "a : TEX X. B(X) <-> (EX X. a:B(X))" unfolding simp_type_defs by blast+ -ML {* -ML_Thms.bind_thms ("case_rls", XH_to_Es @{thms XHs}); -*} +ML {* ML_Thms.bind_thms ("case_rls", XH_to_Es @{thms XHs}) *} subsection {* Canonical Type Rules *}