author | nipkow |
Fri, 07 Jan 1994 14:23:13 +0100 | |
changeset 32 | 4ea58120ef3d |
parent 31 | 04f43a28c97a |
child 33 | 70d46a081b47 |
simpdata.ML | file | annotate | diff | comparison | revisions |
--- 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;