# HG changeset patch
# User blanchet
# Date 1401445671 -7200
# Node ID b5324647e0f12400186e2d5dbe8cef6aa5259697
# Parent  5f69b8c3af5a3b7fcef9a6f56a16177148397fb0
tuned whitespace, to make datatype definitions slightly less intimidating

diff -r 5f69b8c3af5a -r b5324647e0f1 src/HOL/BNF_Examples/ListF.thy
--- a/src/HOL/BNF_Examples/ListF.thy	Fri May 30 12:27:51 2014 +0200
+++ b/src/HOL/BNF_Examples/ListF.thy	Fri May 30 12:27:51 2014 +0200
@@ -14,6 +14,7 @@
 
 datatype_new 'a listF (map: mapF rel: relF) =
   NilF (defaults tlF: NilF) | Conss (hdF: 'a) (tlF: "'a listF")
+
 datatype_compat listF
 
 definition Singll ("[[_]]") where
diff -r 5f69b8c3af5a -r b5324647e0f1 src/HOL/List.thy
--- 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]:
diff -r 5f69b8c3af5a -r b5324647e0f1 src/HOL/Option.thy
--- a/src/HOL/Option.thy	Fri May 30 12:27:51 2014 +0200
+++ b/src/HOL/Option.thy	Fri May 30 12:27:51 2014 +0200
@@ -11,6 +11,7 @@
 datatype_new 'a option =
     None
   | Some (the: 'a)
+
 datatype_compat option
 
 lemma [case_names None Some, cases type: option]: