--- a/src/HOL/MicroJava/BV/BVExample.thy Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/MicroJava/BV/BVExample.thy Mon Mar 01 13:40:23 2010 +0100
@@ -167,8 +167,7 @@
@{prop [display] "P n"}
*}
-constdefs
- intervall :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" ("_ \<in> [_, _')")
+definition intervall :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" ("_ \<in> [_, _')") where
"x \<in> [a, b) \<equiv> a \<le> x \<and> x < b"
lemma pc_0: "x < n \<Longrightarrow> (x \<in> [0, n) \<Longrightarrow> P x) \<Longrightarrow> P x"
@@ -238,8 +237,7 @@
lemmas eff_simps [simp] = eff_def norm_eff_def xcpt_eff_def
declare appInvoke [simp del]
-constdefs
- phi_append :: method_type ("\<phi>\<^sub>a")
+definition phi_append :: method_type ("\<phi>\<^sub>a") where
"\<phi>\<^sub>a \<equiv> map (\<lambda>(x,y). Some (x, map OK y)) [
( [], [Class list_name, Class list_name]),
( [Class list_name], [Class list_name, Class list_name]),
@@ -301,8 +299,7 @@
abbreviation Ctest :: ty
where "Ctest == Class test_name"
-constdefs
- phi_makelist :: method_type ("\<phi>\<^sub>m")
+definition phi_makelist :: method_type ("\<phi>\<^sub>m") where
"\<phi>\<^sub>m \<equiv> map (\<lambda>(x,y). Some (x, y)) [
( [], [OK Ctest, Err , Err ]),
( [Clist], [OK Ctest, Err , Err ]),
@@ -376,8 +373,7 @@
done
text {* The whole program is welltyped: *}
-constdefs
- Phi :: prog_type ("\<Phi>")
+definition Phi :: prog_type ("\<Phi>") where
"\<Phi> C sg \<equiv> if C = test_name \<and> sg = (makelist_name, []) then \<phi>\<^sub>m else
if C = list_name \<and> sg = (append_name, [Class list_name]) then \<phi>\<^sub>a else []"