Session HOL-IMP

Theories

• Permanent_Interpretation
• While_Combinator
• Char_ord
• List_lexord
• Quotient_Syntax
• Quotient_Set
• Quotient_Product
• Quotient_Option
• Quotient_List
• Simps_Case_Conv
• Extended
• 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
• VCG
• Hoare_Sound_Complete
• Hoare_Total
• 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
• Complete_Lattice_ix
• ACom_ITP
• Collecting_ITP
• Abs_Int0_ITP
• Abs_State_ITP
• Abs_Int1_ITP
• Abs_Int1_parity_ITP
• Abs_Int1_const_ITP
• Abs_Int2_ITP
• Abs_Int2_ivl_ITP
• Abs_Int3_ITP
• Abs_Int_den0_fun
• Abs_State_den
• Abs_Int_den0
• Abs_Int_den0_const
• Abs_Int_den1
• Abs_Int_den1_ivl
• Abs_Int_den2
• Procs
• Procs_Dyn_Vars_Dyn
• Procs_Stat_Vars_Dyn
• Procs_Stat_Vars_Stat
• C_like
• OO