isabelle: src/HOL/IMP/ROOT.ML@21c42b095c84 (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",
47602 3d44790b5ab0 reorganised IMP nipkow parents: 46345 diff changeset	3	"~~/src/HOL/Library/While_Combinator",
44932 7c93ee993cae revised AbsInt and added widening and narrowing nipkow parents: 44656 diff changeset	4	"~~/src/HOL/Library/Char_ord", "~~/src/HOL/Library/List_lexord"
7c93ee993cae revised AbsInt and added widening and narrowing nipkow parents: 44656 diff changeset	5	];
44656 22bbd0d1b943 Added Abstract Interpretation theories nipkow parents: 44070 diff changeset	6
43141 11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	7	use_thys
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	8	["BExp",
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	9	"ASM",
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	10	"Small_Step",
43143 1aeafba76f21 Fixed denotational semantics nipkow parents: 43141 diff changeset	11	"Denotation",
43438 a666b8d11252 IMP compiler with int, added reverse soundness direction kleing parents: 43158 diff changeset	12	"Comp_Rev",
43158 686fa0a0696e imported rest of new IMP kleing parents: 43150 diff changeset	13	"Poly_Types",
43141 11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	14	"Sec_Typing",
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	15	"Sec_TypingT",
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	16	"Def_Ass_Sound_Big",
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	17	"Def_Ass_Sound_Small",
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	18	"Live",
45812 0b02adadf384 added IMP/Live_True.thy nipkow parents: 45655 diff changeset	19	"Live_True",
43141 11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	20	"Hoare_Examples",
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	21	"VC",
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	22	"HoareT",
45655 a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step nipkow parents: 45111 diff changeset	23	"Collecting1",
a49f9428aba4 simplified Collecting1 and renamed: step -> step', step_cs -> step nipkow parents: 45111 diff changeset	24	"Collecting_list",
47602 3d44790b5ab0 reorganised IMP nipkow parents: 46345 diff changeset	25	"Abs_Int_Tests",
47613 e72e44cee6f2 added revised version of Abs_Int nipkow parents: 47602 diff changeset	26	"Abs_Int1_parity",
e72e44cee6f2 added revised version of Abs_Int nipkow parents: 47602 diff changeset	27	"Abs_Int1_const",
e72e44cee6f2 added revised version of Abs_Int nipkow parents: 47602 diff changeset	28	"Abs_Int3",
47602 3d44790b5ab0 reorganised IMP nipkow parents: 46345 diff changeset	29	"Abs_Int_ITP/Abs_Int1_parity_ITP",
3d44790b5ab0 reorganised IMP nipkow parents: 46345 diff changeset	30	"Abs_Int_ITP/Abs_Int1_const_ITP",
3d44790b5ab0 reorganised IMP nipkow parents: 46345 diff changeset	31	"Abs_Int_ITP/Abs_Int3_ITP",
45111 054a9ac0d7ef Added Hoare-like Abstract Interpretation nipkow parents: 45110 diff changeset	32	"Abs_Int_Den/Abs_Int_den2",
43141 11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	33	"Procs_Dyn_Vars_Dyn",
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	34	"Procs_Stat_Vars_Dyn",
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	35	"Procs_Stat_Vars_Stat",
11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	36	"C_like",
44070 cebb7abb54b1 import constant folding theory into IMP kleing parents: 43438 diff changeset	37	"OO",
cebb7abb54b1 import constant folding theory into IMP kleing parents: 43438 diff changeset	38	"Fold"
43141 11fce8564415 Replacing old IMP with new Semantics material nipkow parents: 41589 diff changeset	39	];

author	wenzelm
	Sun, 20 May 2012 11:34:33 +0200
changeset 47884	21c42b095c84
parent 47613	e72e44cee6f2
permissions	-rw-r--r--