--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Tue Sep 28 12:47:55 2010 +0200
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy Tue Sep 28 12:47:55 2010 +0200
@@ -18,11 +18,11 @@
section {* Executability of @{term check_bounded} *}
-consts
- list_all'_rec :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> bool"
-primrec
+
+primrec list_all'_rec :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> nat \<Rightarrow> 'a list \<Rightarrow> bool"
+where
"list_all'_rec P n [] = True"
- "list_all'_rec P n (x#xs) = (P x n \<and> list_all'_rec P (Suc n) xs)"
+| "list_all'_rec P n (x#xs) = (P x n \<and> list_all'_rec P (Suc n) xs)"
definition list_all' :: "('a \<Rightarrow> nat \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
"list_all' P xs \<equiv> list_all'_rec P 0 xs"