author | nipkow |
Tue, 20 Sep 2011 05:48:23 +0200 | |
changeset 45015 | fdac1e9880eb |
parent 44932 | 7c93ee993cae |
child 45110 | 305f83b6da54 |
permissions | -rw-r--r-- |
no_document use_thys ["~~/src/HOL/ex/Interpretation_with_Defs", "~~/src/HOL/Library/Char_ord", "~~/src/HOL/Library/List_lexord" ]; use_thys ["BExp", "ASM", "Small_Step", "Denotation", "Comp_Rev", "Poly_Types", "Sec_Typing", "Sec_TypingT", "Def_Ass_Sound_Big", "Def_Ass_Sound_Small", "Live", "AbsInt2", "Hoare_Examples", "VC", "HoareT", "Procs_Dyn_Vars_Dyn", "Procs_Stat_Vars_Dyn", "Procs_Stat_Vars_Stat", "C_like", "OO", "Fold" ];