src/HOLCF/Fixrec.thy
changeset 16463 342d74ca8815
parent 16460 72a08d509d62
child 16551 7abf8a713613
     1.1 --- a/src/HOLCF/Fixrec.thy	Sat Jun 18 00:33:27 2005 +0200
     1.2 +++ b/src/HOLCF/Fixrec.thy	Sat Jun 18 00:38:18 2005 +0200
     1.3 @@ -179,10 +179,16 @@
     1.4  lemma cpair_eqD2: "<x,y> = <x',y'> \<Longrightarrow> y = y'"
     1.5  by simp
     1.6  
     1.7 +text {* lemma for proving rewrite rules *}
     1.8 +
     1.9 +lemma ssubst_lhs: "\<lbrakk>t = s; P s = Q\<rbrakk> \<Longrightarrow> P t = Q"
    1.10 +by simp
    1.11 +
    1.12  ML {*
    1.13  val cpair_equalI = thm "cpair_equalI";
    1.14  val cpair_eqD1 = thm "cpair_eqD1";
    1.15  val cpair_eqD2 = thm "cpair_eqD2";
    1.16 +val ssubst_lhs = thm "ssubst_lhs";
    1.17  *}
    1.18  
    1.19  subsection {* Intitializing the fixrec package *}