src/HOL/MicroJava/BV/BVExample.thy

 
   @{text "\<dots>"}
 
   @{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"
   by (simp add: intervall_def)
 

   and @{term makelist_name} in class @{term test_name}:
 *}
 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]),
    (                     [Class list_name], [Class list_name, Class list_name]),
    (    [Class list_name, Class list_name], [Class list_name, Class list_name]),

 abbreviation Clist :: ty 
   where "Clist == Class list_name"
 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     ]),
     (                       [Clist, Clist], [OK Ctest, Err     , Err     ]),
     (                              [Clist], [OK Clist, Err     , Err     ]),

   apply (simp add: app_def xcpt_app_def) 
   apply simp
   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 []"
 
 lemma wf_prog:
   "wt_jvm_prog E \<Phi>"