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.
dropped junk
authorhaftmann
Tue, 31 Oct 2006 09:29:01 +0100
changeset 21115 f4e79a09c305
parent 21114 3c09ec7565ed
child 21116 be58cded79da
dropped junk
src/HOL/Library/ExecutableRat.thy file | annotate | diff | comparison | revisions
src/HOL/Library/ExecutableSet.thy file | annotate | diff | comparison | revisions 
--- 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
--- 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
isabelle