| changeset 52137 | 7f7337447b1b |
| parent 51717 | 9e7d1c139569 |
| child 58249 | 180f1b3508ed |
--- a/src/HOL/IMPP/Hoare.thy Fri May 24 23:57:24 2013 +0200 +++ b/src/HOL/IMPP/Hoare.thy Fri May 24 23:57:24 2013 +0200 @@ -189,7 +189,7 @@ apply fast done -lemma constant: "[| C ==> G|-{P}.c.{Q} |] ==> G|-{%Z s. P Z s & C}.c.{Q}" +lemma "constant": "[| C ==> G|-{P}.c.{Q} |] ==> G|-{%Z s. P Z s & C}.c.{Q}" apply (rule hoare_derivs.conseq) apply fast done