author | nipkow |
Wed, 14 Sep 2011 06:49:01 +0200 | |
changeset 44923 | b80108b346a9 |
parent 44656 | 22bbd0d1b943 |
child 44932 | 7c93ee993cae |
permissions | -rw-r--r-- |
no_document use_thys ["~~/src/HOL/ex/Interpretation_with_Defs"]; use_thys ["BExp", "ASM", "Small_Step", "Denotation", "Comp_Rev", "Poly_Types", "Sec_Typing", "Sec_TypingT", "Def_Ass_Sound_Big", "Def_Ass_Sound_Small", "Live", "AbsInt1_ivl", "Hoare_Examples", "VC", "HoareT", "Procs_Dyn_Vars_Dyn", "Procs_Stat_Vars_Dyn", "Procs_Stat_Vars_Stat", "C_like", "OO", "Fold" ];