src/HOL/Quotient_Examples/Lift_FSet.thy

--- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Tue May 14 21:56:19 2013 +0200
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Wed May 15 12:10:39 2013 +0200
@@ -35,8 +35,7 @@
 
 subsection {* Lifted constant definitions *}
 
-lift_definition fnil :: "'a fset" ("{||}") is "[]" parametric Nil_transfer
-  by simp
+lift_definition fnil :: "'a fset" ("{||}") is "[]" parametric Nil_transfer .
 
 lift_definition fcons :: "'a \<Rightarrow> 'a fset \<Rightarrow> 'a fset" is Cons parametric Cons_transfer
   by simp