Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
use quot_del instead of ML code in Rat.thy
authorkuncar
Mon, 21 May 2012 16:37:28 +0200
changeset 47952 36a8c477dae8
parent 47951 8c8a03765de7
child 47953 a2c3706c4cb1
use quot_del instead of ML code in Rat.thy
src/HOL/Rat.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Rat.thy	Mon May 21 16:36:48 2012 +0200
+++ b/src/HOL/Rat.thy	Mon May 21 16:37:28 2012 +0200
@@ -1125,7 +1125,6 @@
 
 text {* De-register @{text "rat"} as a quotient type: *}
 
-setup {* Context.theory_map (Lifting_Info.update_quotients @{type_name rat}
-  {quot_thm = @{thm identity_quotient [where 'a=rat]}}) *}
+declare Quotient_rat[quot_del]
 
 end
isabelle