author | nipkow |
Wed, 01 Jun 2011 22:42:37 +0200 | |
changeset 43143 | 1aeafba76f21 |
parent 43141 | 11fce8564415 |
child 43150 | 69bc4dafcc53 |
permissions | -rw-r--r-- |
43141 | 1 |
use_thys |
2 |
["BExp", |
|
3 |
"ASM", |
|
4 |
"Small_Step", |
|
43143 | 5 |
"Denotation", |
43141 | 6 |
"Compiler"(*, |
7 |
"Poly_Types", |
|
8 |
"Sec_Typing", |
|
9 |
"Sec_TypingT", |
|
10 |
"Def_Ass_Sound_Big", |
|
11 |
"Def_Ass_Sound_Small", |
|
12 |
"Def_Ass2_Sound_Small", |
|
13 |
"Def_Ass2_Big0", |
|
14 |
"Live", |
|
15 |
"Hoare_Examples", |
|
16 |
"VC", |
|
17 |
"HoareT", |
|
18 |
"Procs_Dyn_Vars_Dyn", |
|
19 |
"Procs_Stat_Vars_Dyn", |
|
20 |
"Procs_Stat_Vars_Stat", |
|
21 |
"C_like", |
|
22 |
"OO" |
|
924
806721cfbf46
new version of HOL/IMP with curried function application
clasohm
parents:
diff
changeset
|
23 |
*) |
43141 | 24 |
]; |