# HG changeset patch
# User bulwahn
# Date 1327504068 -3600
# Node ID 46c2c96f5d92f7690149f090708d196114336b64
# Parent  f62f5f1fda3b9b4cd99d813d2c044362f8c70e25
adding very basic code generation to Wellfounded theory

diff -r f62f5f1fda3b -r 46c2c96f5d92 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Wed Jan 25 16:07:41 2012 +0100
+++ b/src/HOL/Wellfounded.thy	Wed Jan 25 16:07:48 2012 +0100
@@ -615,6 +615,13 @@
 
 lemmas acc_subset_induct = accp_subset_induct [to_set]
 
+text {* Very basic code generation setup *}
+
+declare accp.simps[code]
+
+lemma [code_unfold]:
+  "(x : acc r) = accp (%x xa. (x, xa) : r) x"
+by (simp add: accp_acc_eq)
 
 subsection {* Tools for building wellfounded relations *}