added let_weak_cong
authornipkow
Fri, 07 Jan 1994 14:23:13 +0100
changeset 32 4ea58120ef3d
parent 31 04f43a28c97a
child 33 70d46a081b47
added let_weak_cong
simpdata.ML
--- 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;