src/HOL/Isar_examples/Hoare.thy
changeset 21404 eb85850d3eb7
parent 21226 a607ae87ee81
child 21588 cd0dc678a205
     1.1 --- a/src/HOL/Isar_examples/Hoare.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/Isar_examples/Hoare.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -32,7 +32,7 @@
     1.4    | While "'a bexp" "'a assn" "'a com"
     1.5  
     1.6  abbreviation
     1.7 -  Skip  ("SKIP")
     1.8 +  Skip  ("SKIP") where
     1.9    "SKIP == Basic id"
    1.10  
    1.11  types