--- a/src/HOL/Real/PReal.thy Tue Jun 10 15:30:54 2008 +0200
+++ b/src/HOL/Real/PReal.thy Tue Jun 10 15:30:56 2008 +0200
@@ -19,7 +19,7 @@
definition
cut :: "rat set => bool" where
- "cut A = ({} \<subset> A &
+ [code func del]: "cut A = ({} \<subset> A &
A < {r. 0 < r} &
(\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u))))"
@@ -56,7 +56,7 @@
definition
diff_set :: "[rat set,rat set] => rat set" where
- "diff_set A B = {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
+ [code func del]: "diff_set A B = {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
definition
mult_set :: "[rat set,rat set] => rat set" where
@@ -64,17 +64,17 @@
definition
inverse_set :: "rat set => rat set" where
- "inverse_set A = {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
+ [code func del]: "inverse_set A = {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
instantiation preal :: "{ord, plus, minus, times, inverse, one}"
begin
definition
- preal_less_def:
+ preal_less_def [code func del]:
"R < S == Rep_preal R < Rep_preal S"
definition
- preal_le_def:
+ preal_le_def [code func del]:
"R \<le> S == Rep_preal R \<subseteq> Rep_preal S"
definition