# HG changeset patch
# User haftmann
# Date 1162283341 -3600
# Node ID f4e79a09c3057611490b8093705a79af918469f0
# Parent  3c09ec7565edfd6283d77f8ca3c4d0c0907e4ee5
dropped junk

diff -r 3c09ec7565ed -r f4e79a09c305 src/HOL/Library/ExecutableRat.thy
--- a/src/HOL/Library/ExecutableRat.thy	Tue Oct 31 09:28:57 2006 +0100
+++ b/src/HOL/Library/ExecutableRat.thy	Tue Oct 31 09:29:01 2006 +0100
@@ -167,10 +167,4 @@
   Orderings.less_eq :: "rat \<Rightarrow> rat \<Rightarrow> bool" ("{*op <= :: erat \<Rightarrow> erat \<Rightarrow> bool*}")
   "op =" :: "rat \<Rightarrow> rat \<Rightarrow> bool" ("{*eq_erat*}")
 
-code_gen
-  of_quotient
-  "0::erat"
-  "1::erat"
-  "op + :: erat \<Rightarrow> erat \<Rightarrow> erat"
-
 end
diff -r 3c09ec7565ed -r f4e79a09c305 src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Tue Oct 31 09:28:57 2006 +0100
+++ b/src/HOL/Library/ExecutableSet.thy	Tue Oct 31 09:29:01 2006 +0100
@@ -271,7 +271,7 @@
   "Bex (xs \<Colon> 'a\<Colon>type set) = Bex xs" ..
 
 code_abstype "'a set" "'a list" where
-  "{}" \<equiv> "empty_list"
+  "{}" \<equiv> empty_list
   insert \<equiv> insertl
   "op \<union>" \<equiv> unionl
   "op \<inter>" \<equiv> intersect