Session HOL-IMP

Theories

• AExp
• BExp
• ASM
• Star
• Com
• Big_Step
• Small_Step
• Finite_Reachable
• Denotational
• Compiler
• Compiler2
• Types
• Poly_Types
• Sec_Type_Expr
• Sec_Typing
• Sec_TypingT
• Vars
• Def_Init_Exp
• Def_Init
• Def_Init_Big
• Def_Init_Small
• Sem_Equiv
• Fold
• Live
• Live_True
• Hoare
• Hoare_Examples
• Hoare_Sound_Complete
• VCG
• Hoare_Total
• Hoare_Total_EX
• VCG_Total_EX
• Hoare_Total_EX2
• VCG_Total_EX2
• Complete_Lattice
• ACom
• Collecting
• Collecting1
• Collecting_Examples
• Abs_Int_Tests
• Abs_Int_init
• Abs_Int0
• Abs_State
• Abs_Int1
• Abs_Int1_parity
• Abs_Int1_const
• Abs_Int2
• Abs_Int2_ivl
• Abs_Int3
• Procs
• Procs_Dyn_Vars_Dyn
• Procs_Stat_Vars_Dyn
• Procs_Stat_Vars_Stat
• C_like
• OO