# HG changeset patch
# User bulwahn
# Date 1283853113 -7200
# Node ID 5ab54bf226acdb4d5baff4236ce7e45ef9ef481f
# Parent  c8406125193be95c6d0786e285ff2a165b226849
renewing specification in example file; adding invocation in example file

diff -r c8406125193b -r 5ab54bf226ac src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Tue Sep 07 11:51:53 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Tue Sep 07 11:51:53 2010 +0200
@@ -810,8 +810,7 @@
  (let (y', x') = f i y x; (y'', xs') = fold_map_idx f (Suc i) y' xs
  in (y'', x' # xs'))"
 
-text {* mode analysis explores thousand modes - this is infeasible at the moment... *}
-(*code_pred [inductify, show_steps] fold_map_idx .*)
+code_pred [inductify] fold_map_idx .
 
 subsection {* Minimum *}
 
@@ -939,10 +938,10 @@
 "height ET = 0"
 | "height (MKT x l r h) = max (height l) (height r) + 1"
 
-consts avl :: "'a tree => bool"
-primrec
+primrec avl :: "'a tree => bool"
+where
   "avl ET = True"
-  "avl (MKT x l r h) = ((height l = height r \<or> height l = 1 + height r \<or> height r = 1+height l) \<and> 
+| "avl (MKT x l r h) = ((height l = height r \<or> height l = 1 + height r \<or> height r = 1+height l) \<and> 
   h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
 (*
 code_pred [inductify] avl .