src/HOL/IMP/Abs_State.thy

--- a/src/HOL/IMP/Abs_State.thy	Tue May 14 21:56:19 2013 +0200
+++ b/src/HOL/IMP/Abs_State.thy	Wed May 15 12:10:39 2013 +0200
@@ -102,8 +102,7 @@
 lift_definition sup_st :: "'a st \<Rightarrow> 'a st \<Rightarrow> 'a st" is "map2_st_rep (op \<squnion>)"
 by (simp add: eq_st_def)
 
-lift_definition top_st :: "'a st" is "[]"
-by(simp add: eq_st_def)
+lift_definition top_st :: "'a st" is "[]" .
 
 instance
 proof