# HG changeset patch
# User nipkow
# Date 1366365897 -7200
# Node ID cdc05fc4cd0decaab7b6a79b2d46c508ba77b06e
# Parent  0c944215934ad94b6328430de884ce992eb286bb
tuned

diff -r 0c944215934a -r cdc05fc4cd0d src/HOL/IMP/Abs_State.thy
--- a/src/HOL/IMP/Abs_State.thy	Thu Apr 18 21:31:24 2013 +0200
+++ b/src/HOL/IMP/Abs_State.thy	Fri Apr 19 12:04:57 2013 +0200
@@ -17,6 +17,8 @@
 definition eq_st :: "('a::top) st_rep \<Rightarrow> 'a st_rep \<Rightarrow> bool" where
 "eq_st S1 S2 = (fun_rep S1 = fun_rep S2)"
 
+hide_type st  --"hide previous def to avoid long names"
+
 quotient_type 'a st = "('a::top) st_rep" / eq_st
 by (metis eq_st_def equivpI reflpI sympI transpI)