src/HOL/IMP/ROOT.ML
author nipkow
Thu, 19 Apr 2012 17:32:30 +0200
changeset 47602 3d44790b5ab0
parent 46345 202f8b8086a3
child 47613 e72e44cee6f2
permissions -rw-r--r--
reorganised IMP

no_document use_thys
  ["~~/src/HOL/ex/Interpretation_with_Defs",
   "~~/src/HOL/Library/While_Combinator",
   "~~/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",
 "Live_True",
 "Hoare_Examples",
 "VC",
 "HoareT",
 "Collecting1",
 "Collecting_list",
 "Abs_Int_Tests",
 "Abs_Int_ITP/Abs_Int1_parity_ITP",
 "Abs_Int_ITP/Abs_Int1_const_ITP",
 "Abs_Int_ITP/Abs_Int3_ITP",
 "Abs_Int_Den/Abs_Int_den2",
 "Procs_Dyn_Vars_Dyn",
 "Procs_Stat_Vars_Dyn",
 "Procs_Stat_Vars_Stat",
 "C_like",
 "OO",
 "Fold"
];