isabelle: src/HOL/Hoare/Examples.thy@608483c2122a (annotated)

1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1374 diff changeset	1	(* Title: HOL/Hoare/Examples.thy
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	2	ID: $Id$
1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1374 diff changeset	3	Author: Norbert Galm
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	4	Copyright 1995 TUM
5e1c0540f285 New directory. nipkow parents: diff changeset	5
5e1c0540f285 New directory. nipkow parents: diff changeset	6	Various arithmetic examples.
5e1c0540f285 New directory. nipkow parents: diff changeset	7	*)
5e1c0540f285 New directory. nipkow parents: diff changeset	8
5e1c0540f285 New directory. nipkow parents: diff changeset	9	Examples = Hoare + Arith2 +
5e1c0540f285 New directory. nipkow parents: diff changeset	10
5e1c0540f285 New directory. nipkow parents: diff changeset	11	syntax
1476 608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1374 diff changeset	12	"@1" :: nat ("1")
608483c2122a expanded tabs; incorporated Konrad's changes clasohm parents: 1374 diff changeset	13	"@2" :: nat ("2")
1335 5e1c0540f285 New directory. nipkow parents: diff changeset	14
5e1c0540f285 New directory. nipkow parents: diff changeset	15	translations
5e1c0540f285 New directory. nipkow parents: diff changeset	16	"1" == "Suc(0)"
5e1c0540f285 New directory. nipkow parents: diff changeset	17	"2" == "Suc(Suc(0))"
5e1c0540f285 New directory. nipkow parents: diff changeset	18	end
5e1c0540f285 New directory. nipkow parents: diff changeset	19
5e1c0540f285 New directory. nipkow parents: diff changeset	20

author	clasohm
	Mon, 05 Feb 1996 21:29:06 +0100
changeset 1476	608483c2122a
parent 1374	5e407f2a3323
child 1625	40501958d0f6
permissions	-rw-r--r--