--- 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