src/HOL/IMP/ROOT.ML
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 45111 054a9ac0d7ef
child 45655 a49f9428aba4
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
nipkow@44932
     1
no_document use_thys
nipkow@44932
     2
  ["~~/src/HOL/ex/Interpretation_with_Defs",
nipkow@44932
     3
   "~~/src/HOL/Library/Char_ord", "~~/src/HOL/Library/List_lexord"
nipkow@44932
     4
  ];
nipkow@44656
     5
nipkow@43141
     6
use_thys
nipkow@43141
     7
["BExp",
nipkow@43141
     8
 "ASM",
nipkow@43141
     9
 "Small_Step",
nipkow@43143
    10
 "Denotation",
kleing@43438
    11
 "Comp_Rev",
kleing@43158
    12
 "Poly_Types",
nipkow@43141
    13
 "Sec_Typing",
nipkow@43141
    14
 "Sec_TypingT",
nipkow@43141
    15
 "Def_Ass_Sound_Big",
nipkow@43141
    16
 "Def_Ass_Sound_Small",
nipkow@43141
    17
 "Live",
nipkow@43141
    18
 "Hoare_Examples",
nipkow@43141
    19
 "VC",
nipkow@43141
    20
 "HoareT",
nipkow@45111
    21
 "Abs_Int2",
nipkow@45111
    22
 "Abs_Int_Den/Abs_Int_den2",
nipkow@43141
    23
 "Procs_Dyn_Vars_Dyn",
nipkow@43141
    24
 "Procs_Stat_Vars_Dyn",
nipkow@43141
    25
 "Procs_Stat_Vars_Stat",
nipkow@43141
    26
 "C_like",
kleing@44070
    27
 "OO",
kleing@44070
    28
 "Fold"
nipkow@43141
    29
];