# HG changeset patch # User wenzelm # Date 1526846686 -7200 # Node ID eb57621568bb001175ffaa5e160e92fd89e3e6ac # Parent e7c85e2dc1988646a33c069e91c6a59b3fa6c572 avoid undeclared frees; diff -r e7c85e2dc198 -r eb57621568bb src/Doc/Tutorial/Rules/Forward.thy --- a/src/Doc/Tutorial/Rules/Forward.thy Sun May 20 22:04:17 2018 +0200 +++ b/src/Doc/Tutorial/Rules/Forward.thy Sun May 20 22:04:46 2018 +0200 @@ -55,14 +55,14 @@ \ -lemmas gcd_mult_0 = gcd_mult_distrib2 [of k 1] +lemmas gcd_mult_0 = gcd_mult_distrib2 [of k 1] for k lemmas gcd_mult_1 = gcd_mult_0 [simplified] lemmas where1 = gcd_mult_distrib2 [where m=1] lemmas where2 = gcd_mult_distrib2 [where m=1 and k=1] -lemmas where3 = gcd_mult_distrib2 [where m=1 and k="j+k"] +lemmas where3 = gcd_mult_distrib2 [where m=1 and k="j+k"] for j k text \ example using ``of'': @@ -87,7 +87,7 @@ lemmas gcd_mult0 = gcd_mult_1 [THEN sym] (*not quite right: we need ?k but this gives k*) -lemmas gcd_mult0' = gcd_mult_distrib2 [of k 1, simplified, THEN sym] +lemmas gcd_mult0' = gcd_mult_distrib2 [of k 1, simplified, THEN sym] for k (*better in one step!*) text \ @@ -98,7 +98,7 @@ by (rule gcd_mult_distrib2 [of k 1, simplified, THEN sym]) -lemmas gcd_self0 = gcd_mult [of k 1, simplified] +lemmas gcd_self0 = gcd_mult [of k 1, simplified] for k text \ diff -r e7c85e2dc198 -r eb57621568bb src/HOL/UNITY/Constrains.thy --- a/src/HOL/UNITY/Constrains.thy Sun May 20 22:04:17 2018 +0200 +++ b/src/HOL/UNITY/Constrains.thy Sun May 20 22:04:46 2018 +0200 @@ -387,7 +387,7 @@ (*Delete the nearest invariance assumption (which will be the second one used by Always_Int_I) *) -lemmas Always_thin = thin_rl [of "F \ Always A"] +lemmas Always_thin = thin_rl [of "F \ Always A"] for F A subsection\Totalize\