--- a/src/HOL/NSA/StarDef.thy Mon Jul 12 08:58:12 2010 +0200
+++ b/src/HOL/NSA/StarDef.thy Mon Jul 12 08:58:13 2010 +0200
@@ -290,7 +290,7 @@
subsection {* Internal predicates *}
definition unstar :: "bool star \<Rightarrow> bool" where
- [code del]: "unstar b \<longleftrightarrow> b = star_of True"
+ "unstar b \<longleftrightarrow> b = star_of True"
lemma unstar_star_n: "unstar (star_n P) = ({n. P n} \<in> \<U>)"
by (simp add: unstar_def star_of_def star_n_eq_iff)
@@ -431,7 +431,7 @@
begin
definition
- star_zero_def [code del]: "0 \<equiv> star_of 0"
+ star_zero_def: "0 \<equiv> star_of 0"
instance ..
@@ -441,7 +441,7 @@
begin
definition
- star_one_def [code del]: "1 \<equiv> star_of 1"
+ star_one_def: "1 \<equiv> star_of 1"
instance ..
@@ -451,7 +451,7 @@
begin
definition
- star_add_def [code del]: "(op +) \<equiv> *f2* (op +)"
+ star_add_def: "(op +) \<equiv> *f2* (op +)"
instance ..
@@ -461,7 +461,7 @@
begin
definition
- star_mult_def [code del]: "(op *) \<equiv> *f2* (op *)"
+ star_mult_def: "(op *) \<equiv> *f2* (op *)"
instance ..
@@ -471,7 +471,7 @@
begin
definition
- star_minus_def [code del]: "uminus \<equiv> *f* uminus"
+ star_minus_def: "uminus \<equiv> *f* uminus"
instance ..
@@ -481,7 +481,7 @@
begin
definition
- star_diff_def [code del]: "(op -) \<equiv> *f2* (op -)"
+ star_diff_def: "(op -) \<equiv> *f2* (op -)"
instance ..