author | nipkow |
Sun, 11 Dec 2011 18:22:06 +0100 | |
changeset 45812 | 0b02adadf384 |
parent 45655 | a49f9428aba4 |
child 46345 | 202f8b8086a3 |
permissions | -rw-r--r-- |
44932 | 1 |
no_document use_thys |
2 |
["~~/src/HOL/ex/Interpretation_with_Defs", |
|
3 |
"~~/src/HOL/Library/Char_ord", "~~/src/HOL/Library/List_lexord" |
|
4 |
]; |
|
44656 | 5 |
|
43141 | 6 |
use_thys |
7 |
["BExp", |
|
8 |
"ASM", |
|
9 |
"Small_Step", |
|
43143 | 10 |
"Denotation", |
43438
a666b8d11252
IMP compiler with int, added reverse soundness direction
kleing
parents:
43158
diff
changeset
|
11 |
"Comp_Rev", |
43158 | 12 |
"Poly_Types", |
43141 | 13 |
"Sec_Typing", |
14 |
"Sec_TypingT", |
|
15 |
"Def_Ass_Sound_Big", |
|
16 |
"Def_Ass_Sound_Small", |
|
17 |
"Live", |
|
45812 | 18 |
"Live_True", |
43141 | 19 |
"Hoare_Examples", |
20 |
"VC", |
|
21 |
"HoareT", |
|
45111 | 22 |
"Abs_Int2", |
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", |
45111 | 25 |
"Abs_Int_Den/Abs_Int_den2", |
43141 | 26 |
"Procs_Dyn_Vars_Dyn", |
27 |
"Procs_Stat_Vars_Dyn", |
|
28 |
"Procs_Stat_Vars_Stat", |
|
29 |
"C_like", |
|
44070 | 30 |
"OO", |
31 |
"Fold" |
|
43141 | 32 |
]; |