src/HOL/List.thy
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]: