# HG changeset patch # User wenzelm # Date 978553430 -3600 # Node ID 0deff01974963e48093252fb4b9f9e7029133497 # Parent 115c65650be3aee6d21fab18a3d5a38116cf6219 renamed .sml files to .ML; tuned package setup; diff -r 115c65650be3 -r 0deff0197496 src/HOL/Recdef.thy --- a/src/HOL/Recdef.thy Wed Jan 03 21:23:13 2001 +0100 +++ b/src/HOL/Recdef.thy Wed Jan 03 21:23:50 2001 +0100 @@ -1,22 +1,58 @@ (* Title: HOL/Recdef.thy ID: $Id$ - Author: Konrad Slind + Author: Konrad Slind and Markus Wenzel, TU Muenchen TFL: recursive function definitions. *) theory Recdef = Wellfounded_Relations + Datatype files - "../TFL/utils.sml" - "../TFL/usyntax.sml" - "../TFL/thms.sml" - "../TFL/dcterm.sml" - "../TFL/rules.sml" - "../TFL/thry.sml" - "../TFL/tfl.sml" - "../TFL/post.sml" - "Tools/recdef_package.ML": + ("../TFL/utils.ML") + ("../TFL/usyntax.ML") + ("../TFL/dcterm.ML") + ("../TFL/thms.ML") + ("../TFL/rules.ML") + ("../TFL/thry.ML") + ("../TFL/tfl.ML") + ("../TFL/post.ML") + ("Tools/recdef_package.ML"): + +lemma tfl_some: "\P x. P x --> P (Eps P)" + by (blast intro: someI) + +lemma tfl_eq_True: "(x = True) --> x" + by blast + +lemma tfl_rev_eq_mp: "(x = y) --> y --> x"; + by blast + +lemma tfl_simp_thm: "(x --> y) --> (x = x') --> (x' --> y)" + by blast +lemma tfl_P_imp_P_iff_True: "P ==> P = True" + by blast + +lemma tfl_imp_trans: "(A --> B) ==> (B --> C) ==> (A --> C)" + by blast + +lemma tfl_disj_assoc: "(a \ b) \ c == a \ (b \ c)" + by simp + +lemma tfl_disjE: "P \ Q ==> P --> R ==> Q --> R ==> R" + by blast + +lemma tfl_exE: "\x. P x ==> \x. P x --> Q ==> Q" + by blast + +use "../TFL/utils.ML" +use "../TFL/usyntax.ML" +use "../TFL/dcterm.ML" +use "../TFL/thms.ML" +use "../TFL/rules.ML" +use "../TFL/thry.ML" +use "../TFL/tfl.ML" +use "../TFL/post.ML" +use "Tools/recdef_package.ML" setup RecdefPackage.setup lemmas [recdef_simp] =