src/HOL/HOL.thy
changeset 27572 67cd6ed76446
parent 27338 2cd6c60cc10b
child 28012 2308843f8b66
     1.1 --- a/src/HOL/HOL.thy	Mon Jul 14 17:02:55 2008 +0200
     1.2 +++ b/src/HOL/HOL.thy	Mon Jul 14 17:47:18 2008 +0200
     1.3 @@ -918,6 +918,8 @@
     1.4    val subst = @{thm subst}
     1.5    val sym = @{thm sym}
     1.6    val thin_refl = @{thm thin_refl};
     1.7 +  val prop_subst = @{lemma "PROP P t ==> PROP prop (x = t ==> PROP P x)"
     1.8 +                     by (unfold prop_def) (drule eq_reflection, unfold)}
     1.9  end);
    1.10  open Hypsubst;
    1.11