# HG changeset patch
# User wenzelm
# Date 968172484 -7200
# Node ID 709a295731e2b18443be17ff39af2da4cd995915
# Parent  a1383b55ac054184112dfa3930cc6a2f62eccad9
improved recdef setup;

diff -r a1383b55ac05 -r 709a295731e2 src/HOL/Recdef.thy
--- a/src/HOL/Recdef.thy	Tue Sep 05 18:47:46 2000 +0200
+++ b/src/HOL/Recdef.thy	Tue Sep 05 18:48:04 2000 +0200
@@ -7,30 +7,38 @@
 
 theory Recdef = WF_Rel + Datatype
 files
-  (*establish a base of common and/or helpful functions*)
-  "../TFL/utils.sig"
-
-  "../TFL/usyntax.sig"
-  "../TFL/rules.sig"
-  "../TFL/thry.sig"
-  "../TFL/thms.sig"
-  "../TFL/tfl.sig"
   "../TFL/utils.sml"
-
-  (*supply implementations*)
   "../TFL/usyntax.sml"
   "../TFL/thms.sml"
   "../TFL/dcterm.sml"
   "../TFL/rules.sml"
   "../TFL/thry.sml"
-
-  (*link system and specialize for Isabelle*)
   "../TFL/tfl.sml"
   "../TFL/post.sml"
-
-  (*theory extender wrapper module*)
   "Tools/recdef_package.ML":
 
 setup RecdefPackage.setup
 
+lemmas [recdef_simp] =
+  inv_image_def
+  measure_def
+  lex_prod_def
+  less_Suc_eq [THEN iffD2]
+
+lemmas [recdef_cong] =
+  if_cong
+
+lemma let_cong [recdef_cong]:
+    "M = N ==> (!!x. x = N ==> f x = g x) ==> Let M f = Let N g"
+  by (unfold Let_def) blast
+
+lemmas [recdef_wf] =
+  wf_trancl
+  wf_less_than
+  wf_lex_prod
+  wf_inv_image
+  wf_measure
+  wf_pred_nat
+  wf_empty
+
 end