src/HOL/ex/Predicate_Compile_ex.thy

 
 inductive append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
     "append [] xs xs"
   | "append xs ys zs \<Longrightarrow> append (x # xs) ys (x # zs)"
 
-code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) [inductify] append .
+code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) append .
 code_pred [depth_limited] append .
 code_pred [rpred] append .
 
 thm append.equation
 thm append.depth_limited_equation

 
 code_pred [rpred] lexn .
 
 thm lexn.rpred_equation
 
-code_pred [inductify] lenlex .
+code_pred [inductify, show_steps] lenlex .
 thm lenlex.equation
 
 code_pred [inductify, rpred] lenlex .
 thm lenlex.rpred_equation
 

 code_pred [inductify] rel_comp .
 thm rel_comp.equation
 code_pred [inductify] Image .
 thm Image.equation
 (*TODO: *)
-(*code_pred [inductify] Id_on .*)
+ML {* Toplevel.debug := true *}
+declare Id_on_def[unfolded UNION_def, code_pred_def]
+
+code_pred [inductify] Id_on .
+thm Id_on.equation
 code_pred [inductify] Domain .
 thm Domain.equation
 code_pred [inductify] Range .
 thm sym_def
 code_pred [inductify] Field .
-(* code_pred [inductify] refl_on .*)
+declare Sigma_def[unfolded UNION_def, code_pred_def]
+declare refl_on_def[unfolded UNION_def, code_pred_def]
+code_pred [inductify] refl_on .
+thm refl_on.equation
 code_pred [inductify] total_on .
 thm total_on.equation
 (*
 code_pred [inductify] sym .
 thm sym.equation