src/HOL/IMP/ROOT.ML
changeset 45812 0b02adadf384
parent 45655 a49f9428aba4
child 46345 202f8b8086a3
equal deleted inserted replaced
45811:f506015ca2dc 45812:0b02adadf384
    13  "Sec_Typing",
    13  "Sec_Typing",
    14  "Sec_TypingT",
    14  "Sec_TypingT",
    15  "Def_Ass_Sound_Big",
    15  "Def_Ass_Sound_Big",
    16  "Def_Ass_Sound_Small",
    16  "Def_Ass_Sound_Small",
    17  "Live",
    17  "Live",
       
    18  "Live_True",
    18  "Hoare_Examples",
    19  "Hoare_Examples",
    19  "VC",
    20  "VC",
    20  "HoareT",
    21  "HoareT",
    21  "Abs_Int2",
    22  "Abs_Int2",
    22  "Collecting1",
    23  "Collecting1",