changeset 55531 | 601ca8efa000 |
parent 55525 | 70b7e91fa1f9 |
child 55564 | e81ee43ab290 |
--- a/src/HOL/List.thy Mon Feb 17 13:31:42 2014 +0100 +++ b/src/HOL/List.thy Mon Feb 17 13:31:42 2014 +0100 @@ -11,8 +11,7 @@ datatype_new 'a list (map: map rel: list_all2) = =: Nil (defaults tl: "[]") ("[]") | Cons (hd: 'a) (tl: "'a list") (infixr "#" 65) - -datatype_new_compat list +datatype_compat list lemma [case_names Nil Cons, cases type: list]: -- {* for backward compatibility -- names of variables differ *}