| changeset 61260 | e6f03fae14d5 |
| parent 61179 | 16775cad1a5c |
| child 61430 | 1efe2f3728a6 |
--- a/src/HOL/IMP/Abs_State.thy Wed Sep 23 09:50:38 2015 +0200 +++ b/src/HOL/IMP/Abs_State.thy Thu Sep 24 13:33:42 2015 +0200 @@ -19,7 +19,7 @@ hide_type st --"hide previous def to avoid long names" -quotient_type 'a st = "('a::top) st_rep" / eq_st +quotient_type (overloaded) 'a st = "('a::top) st_rep" / eq_st morphisms rep_st St by (metis eq_st_def equivpI reflpI sympI transpI)