isabelle: src/HOL/IMP/Com.thy@6cf5e58f1185 (annotated)

43141 11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 42174 diff changeset	1	header "IMP --- A Simple Imperative Language"
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	2
43141 11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 42174 diff changeset	3	theory Com imports BExp begin
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	4
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	5	datatype
43141 11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 42174 diff changeset	6	com = SKIP
45321 b227989b6ee6 more IMP text fragments kleing parents: 45212 diff changeset	7	\| Assign vname aexp ("_ ::= _" [1000, 61] 61)
47818 151d137f1095 renamed Semi to Seq nipkow parents: 45415 diff changeset	8	\| Seq com com ("_;/ _" [60, 61] 60)
43141 11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 42174 diff changeset	9	\| If bexp com com ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61)
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 42174 diff changeset	10	\| While bexp com ("(WHILE _/ DO _)" [0, 61] 61)
924 806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	11
806721cfbf46 new version of HOL/IMP with curried function application clasohm parents: diff changeset	12	end

author	blanchet
	Wed, 18 Jul 2012 08:44:03 +0200
changeset 48302	6cf5e58f1185
parent 47818	151d137f1095
child 52046	bc01725d7918
permissions	-rw-r--r--