diff -r 4dc65845eab3 -r d8d7d1b785af src/HOL/MicroJava/DFA/SemilatAlg.thy
--- a/src/HOL/MicroJava/DFA/SemilatAlg.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/MicroJava/DFA/SemilatAlg.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -9,29 +9,24 @@
 imports Typing_Framework Product
 begin
 
-constdefs 
-  lesubstep_type :: "(nat \<times> 's) list \<Rightarrow> 's ord \<Rightarrow> (nat \<times> 's) list \<Rightarrow> bool"
-                    ("(_ /<=|_| _)" [50, 0, 51] 50)
+definition lesubstep_type :: "(nat \<times> 's) list \<Rightarrow> 's ord \<Rightarrow> (nat \<times> 's) list \<Rightarrow> bool"
+                    ("(_ /<=|_| _)" [50, 0, 51] 50) where
   "x <=|r| y \<equiv> \<forall>(p,s) \<in> set x. \<exists>s'. (p,s') \<in> set y \<and> s <=_r s'"
 
-consts
-  plusplussub :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" ("(_ /++'__ _)" [65, 1000, 66] 65)
-primrec
+primrec plusplussub :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a" ("(_ /++'__ _)" [65, 1000, 66] 65) where
   "[] ++_f y = y"
-  "(x#xs) ++_f y = xs ++_f (x +_f y)"
+| "(x#xs) ++_f y = xs ++_f (x +_f y)"
 
-constdefs
- bounded :: "'s step_type \<Rightarrow> nat \<Rightarrow> bool"
+definition bounded :: "'s step_type \<Rightarrow> nat \<Rightarrow> bool" where
 "bounded step n == !p<n. !s. !(q,t):set(step p s). q<n"  
 
- pres_type :: "'s step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool"
+definition pres_type :: "'s step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool" where
 "pres_type step n A == \<forall>s\<in>A. \<forall>p<n. \<forall>(q,s')\<in>set (step p s). s' \<in> A"
 
- mono :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool"
+definition mono :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> bool" where
 "mono r step n A ==
  \<forall>s p t. s \<in> A \<and> p < n \<and> s <=_r t \<longrightarrow> step p s <=|r| step p t"
 
-
 lemma pres_typeD:
   "\<lbrakk> pres_type step n A; s\<in>A; p<n; (q,s')\<in>set (step p s) \<rbrakk> \<Longrightarrow> s' \<in> A"
   by (unfold pres_type_def, blast)