isabelle: src/HOL/Hoare/Examples.thy@5e407f2a3323 (annotated)

1335 5e1c0540f285 New directory. nipkow parents: diff changeset	1	(* Title: HOL/Hoare/Examples.thy
5e1c0540f285 New directory. nipkow parents: diff changeset	2	ID: $Id$
5e1c0540f285 New directory. nipkow parents: diff changeset	3	Author: Norbert Galm
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
1374 5e407f2a3323 removed quotes from consts and syntax sections clasohm parents: 1335 diff changeset	12	"@1" :: nat ("1")
5e407f2a3323 removed quotes from consts and syntax sections clasohm parents: 1335 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
	Wed, 29 Nov 1995 17:01:41 +0100
changeset 1374	5e407f2a3323
parent 1335	5e1c0540f285
child 1476	608483c2122a
permissions	-rw-r--r--