changeset 57123 | b5324647e0f1 |
parent 57091 | 1fa9c19ba2c9 |
child 57198 | 159e1b043495 |
--- a/src/HOL/List.thy Fri May 30 12:27:51 2014 +0200 +++ b/src/HOL/List.thy Fri May 30 12:27:51 2014 +0200 @@ -8,9 +8,10 @@ imports Presburger Code_Numeral Quotient Lifting_Set Lifting_Option Lifting_Product begin -datatype_new (set: 'a) list (map: map rel: list_all2) = +datatype_new (set: 'a) list (map: map rel: list_all2) = Nil (defaults tl: "[]") ("[]") | Cons (hd: 'a) (tl: "'a list") (infixr "#" 65) + datatype_compat list lemma [case_names Nil Cons, cases type: list]: