isabelle: src/HOL/IMP/ROOT.ML@054a9ac0d7ef (annotated)

44932 7c93ee993cae revised AbsInt and added widening and narrowing nipkow parents: 44656 diff changeset	1	no_document use_thys
7c93ee993cae revised AbsInt and added widening and narrowing nipkow parents: 44656 diff changeset	2	["~~/src/HOL/ex/Interpretation_with_Defs",
7c93ee993cae revised AbsInt and added widening and narrowing nipkow parents: 44656 diff changeset	3	"~~/src/HOL/Library/Char_ord", "~~/src/HOL/Library/List_lexord"
7c93ee993cae revised AbsInt and added widening and narrowing nipkow parents: 44656 diff changeset	4	];
44656 22bbd0d1b943 Added Abstract Interpretation theories nipkow parents: 44070 diff changeset	5
43141 11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	6	use_thys
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	7	["BExp",
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	8	"ASM",
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	9	"Small_Step",
43143 1aeafba76f21 Fixed denotational semantics nipkow parents: 43141 diff changeset	10	"Denotation",
43438 a666b8d11252 IMP compiler with int, added reverse soundness direction kleing parents: 43158 diff changeset	11	"Comp_Rev",
43158 686fa0a0696e imported rest of new IMP kleing parents: 43150 diff changeset	12	"Poly_Types",
43141 11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	13	"Sec_Typing",
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	14	"Sec_TypingT",
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	15	"Def_Ass_Sound_Big",
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	16	"Def_Ass_Sound_Small",
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	17	"Live",
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	18	"Hoare_Examples",
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	19	"VC",
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	20	"HoareT",
45111 054a9ac0d7ef Added Hoare-like Abstract Interpretation nipkow parents: 45110 diff changeset	21	"Abs_Int2",
054a9ac0d7ef Added Hoare-like Abstract Interpretation nipkow parents: 45110 diff changeset	22	"Abs_Int_Den/Abs_Int_den2",
43141 11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	23	"Procs_Dyn_Vars_Dyn",
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	24	"Procs_Stat_Vars_Dyn",
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	25	"Procs_Stat_Vars_Stat",
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	26	"C_like",
44070 cebb7abb54b1 import constant folding theory into IMP kleing parents: 43438 diff changeset	27	"OO",
cebb7abb54b1 import constant folding theory into IMP kleing parents: 43438 diff changeset	28	"Fold"
43141 11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	29	];

author	nipkow
	Wed, 28 Sep 2011 09:55:11 +0200
changeset 45111	054a9ac0d7ef
parent 45110	305f83b6da54
child 45655	a49f9428aba4
permissions	-rw-r--r--