isabelle: src/HOL/IMP/ROOT.ML@f745bcc4a1e5 (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",
45812 0b02adadf384 added IMP/Live_True.thy nipkow parents: 45655 diff changeset	18	"Live_True",
43141 11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	19	"Hoare_Examples",
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	20	"VC",
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	21	"HoareT",
45655 a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step nipkow parents: 45111 diff changeset	22	"Collecting1",
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step nipkow parents: 45111 diff changeset	23	"Collecting_list",
46345 202f8b8086a3 added parity analysis nipkow parents: 45812 diff changeset	24	"Abs_Int0",
202f8b8086a3 added parity analysis nipkow parents: 45812 diff changeset	25	"Abs_Int0_parity",
202f8b8086a3 added parity analysis nipkow parents: 45812 diff changeset	26	"Abs_Int0_const",
202f8b8086a3 added parity analysis nipkow parents: 45812 diff changeset	27	"Abs_Int2",
45111 054a9ac0d7ef Added Hoare-like Abstract Interpretation nipkow parents: 45110 diff changeset	28	"Abs_Int_Den/Abs_Int_den2",
43141 11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	29	"Procs_Dyn_Vars_Dyn",
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	30	"Procs_Stat_Vars_Dyn",
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	31	"Procs_Stat_Vars_Stat",
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	32	"C_like",
44070 cebb7abb54b1 import constant folding theory into IMP kleing parents: 43438 diff changeset	33	"OO",
cebb7abb54b1 import constant folding theory into IMP kleing parents: 43438 diff changeset	34	"Fold"
43141 11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	35	];

author	wenzelm
	Mon, 27 Feb 2012 16:56:25 +0100
changeset 46711	f745bcc4a1e5
parent 46345	202f8b8086a3
child 47602	3d44790b5ab0
permissions	-rw-r--r--