| changeset 1625 | 40501958d0f6 |
| parent 1476 | 608483c2122a |
| child 5646 | 7c2ddbaf8b8c |
--- a/src/HOL/Hoare/Examples.thy Thu Mar 28 10:56:10 1996 +0100 +++ b/src/HOL/Hoare/Examples.thy Thu Mar 28 12:25:55 1996 +0100 @@ -6,15 +6,4 @@ Various arithmetic examples. *) -Examples = Hoare + Arith2 + - -syntax - "@1" :: nat ("1") - "@2" :: nat ("2") - -translations - "1" == "Suc(0)" - "2" == "Suc(Suc(0))" -end - - +Examples = Hoare + Arith2