equal
deleted
inserted
replaced
1 no_document use_thys |
|
2 ["~~/src/HOL/ex/Interpretation_with_Defs", |
|
3 "~~/src/HOL/Library/While_Combinator", |
|
4 "~~/src/HOL/Library/Char_ord", "~~/src/HOL/Library/List_lexord" |
|
5 ]; |
|
6 |
|
7 use_thys |
|
8 ["BExp", |
|
9 "ASM", |
|
10 "Small_Step", |
|
11 "Denotation", |
|
12 "Comp_Rev", |
|
13 "Poly_Types", |
|
14 "Sec_Typing", |
|
15 "Sec_TypingT", |
|
16 "Def_Ass_Sound_Big", |
|
17 "Def_Ass_Sound_Small", |
|
18 "Live", |
|
19 "Live_True", |
|
20 "Hoare_Examples", |
|
21 "VC", |
|
22 "HoareT", |
|
23 "Collecting1", |
|
24 "Collecting_list", |
|
25 "Abs_Int_Tests", |
|
26 "Abs_Int1_parity", |
|
27 "Abs_Int1_const", |
|
28 "Abs_Int3", |
|
29 "Abs_Int_ITP/Abs_Int1_parity_ITP", |
|
30 "Abs_Int_ITP/Abs_Int1_const_ITP", |
|
31 "Abs_Int_ITP/Abs_Int3_ITP", |
|
32 "Abs_Int_Den/Abs_Int_den2", |
|
33 "Procs_Dyn_Vars_Dyn", |
|
34 "Procs_Stat_Vars_Dyn", |
|
35 "Procs_Stat_Vars_Stat", |
|
36 "C_like", |
|
37 "OO", |
|
38 "Fold" |
|
39 ]; |
|