use quot_del instead of ML code in Rat.thy
authorkuncar
Mon May 21 16:37:28 2012 +0200 (2012-05-21)
changeset 4795236a8c477dae8
parent 47951 8c8a03765de7
child 47953 a2c3706c4cb1
use quot_del instead of ML code in Rat.thy
src/HOL/Rat.thy
     1.1 --- a/src/HOL/Rat.thy	Mon May 21 16:36:48 2012 +0200
     1.2 +++ b/src/HOL/Rat.thy	Mon May 21 16:37:28 2012 +0200
     1.3 @@ -1125,7 +1125,6 @@
     1.4  
     1.5  text {* De-register @{text "rat"} as a quotient type: *}
     1.6  
     1.7 -setup {* Context.theory_map (Lifting_Info.update_quotients @{type_name rat}
     1.8 -  {quot_thm = @{thm identity_quotient [where 'a=rat]}}) *}
     1.9 +declare Quotient_rat[quot_del]
    1.10  
    1.11  end