changeset 32 | 4ea58120ef3d |
parent 30 | 2fdeeae553ac |
child 34 | 7d437bed7765 |
--- a/simpdata.ML Fri Jan 07 14:22:37 1994 +0100 +++ b/simpdata.ML Fri Jan 07 14:23:13 1994 +0100 @@ -120,4 +120,9 @@ "b=c ==> if(b,x,y) = if(c,x,y)" (fn [prem] => [rtac (prem RS arg_cong) 1]); +(*Prevents simplification of t: much faster*) +val let_weak_cong = prove_goal HOL.thy + "a = b ==> (let x=a in t(x)) = (let x=b in t(x))" + (fn [prem] => [rtac (prem RS arg_cong) 1]); + end;