isabelle: src/HOL/IMP/Com.thy@7de87f1ae965 (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
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 42174 diff changeset	7	\| Assign name aexp ("_ ::= _" [1000, 61] 61)
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 42174 diff changeset	8	\| Semi com com ("_;/ _" [60, 61] 60)
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	wenzelm
	Sat, 03 Sep 2011 21:15:35 +0200
changeset 44676	7de87f1ae965
parent 43141	11fce8564415
child 45212	e87feee00a4c
permissions	-rw-r--r--