author | nipkow |
Thu, 20 Oct 2011 09:48:00 +0200 | |
changeset 45212 | e87feee00a4c |
parent 45111 | 054a9ac0d7ef |
child 45655 | a49f9428aba4 |
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", "Hoare_Examples", "VC", "HoareT", "Abs_Int2", "Abs_Int_Den/Abs_Int_den2", "Procs_Dyn_Vars_Dyn", "Procs_Stat_Vars_Dyn", "Procs_Stat_Vars_Stat", "C_like", "OO", "Fold" ];