src/HOL/HOL.thy
changeset 15423 761a4f8e6ad6
parent 15411 1d195de59497
child 15481 fc075ae929e4
     1.1 --- a/src/HOL/HOL.thy	Sat Dec 18 17:12:45 2004 +0100
     1.2 +++ b/src/HOL/HOL.thy	Sat Dec 18 17:14:33 2004 +0100
     1.3 @@ -1098,6 +1098,14 @@
     1.4  lemma Eq_TrueI: "P ==> P == True" by (unfold atomize_eq) rules
     1.5  lemma Eq_FalseI: "~P ==> P == False" by (unfold atomize_eq) rules
     1.6  
     1.7 +text {* \medskip let rules for simproc *}
     1.8 +
     1.9 +lemma Let_folded: "f x \<equiv> g x \<Longrightarrow>  Let x f \<equiv> Let x g"
    1.10 +  by (unfold Let_def)
    1.11 +
    1.12 +lemma Let_unfold: "f x \<equiv> g \<Longrightarrow>  Let x f \<equiv> g"
    1.13 +  by (unfold Let_def)
    1.14 +
    1.15  subsubsection {* Actual Installation of the Simplifier *}
    1.16  
    1.17  use "simpdata.ML"