# HG changeset patch
# User wenzelm
# Date 1140643113 -3600
# Node ID e1b6a50713489f4779e4188e2f36bd8efb61baa5
# Parent  d7fd5415a781991f1ff4e70df29e5fdc52f3145c
tuned proofs;

diff -r d7fd5415a781 -r e1b6a5071348 src/HOL/Isar_examples/Hoare.thy
--- a/src/HOL/Isar_examples/Hoare.thy	Wed Feb 22 22:18:32 2006 +0100
+++ b/src/HOL/Isar_examples/Hoare.thy	Wed Feb 22 22:18:33 2006 +0100
@@ -31,10 +31,9 @@
   | Cond "'a bexp" "'a com" "'a com"
   | While "'a bexp" "'a assn" "'a com"
 
-syntax
-  "_skip" :: "'a com"    ("SKIP")
-translations
-  "SKIP" == "Basic id"
+abbreviation (output)
+  Skip  ("SKIP")
+  "SKIP == Basic id"
 
 types
   'a sem = "'a => 'a => bool"
@@ -169,10 +168,10 @@
   then obtain n where "iter n b (Sem c) s s'" by auto
   from this and s show "s' : P Int -b"
   proof (induct n fixing: s)
-    case (0 s)
+    case 0
     thus ?case by auto
   next
-    case (Suc n s)
+    case (Suc n)
     then obtain s'' where b: "s : b" and sem: "Sem c s s''"
       and iter: "iter n b (Sem c) s'' s'"
       by auto