Session Launchbury
View
theory dependencies
View
document
View
outline
Theories
HOL-Library.AList
AList-Utils
HOLCF-Join
HOLCF-Join-Classes
Env
HOL-Library.Infinite_Set
HOL-Library.Cancellation
File ‹Cancellation/cancel.ML›
File ‹Cancellation/cancel_data.ML›
File ‹Cancellation/cancel_simprocs.ML›
HOL-Library.Multiset
File ‹multiset_simprocs.ML›
HOL-Library.FSet
HOL-Library.Phantom_Type
HOL-Library.Cardinality
FinFun.FinFun
Nominal2.Nominal2_Base
File ‹nominal_basics.ML›
File ‹nominal_thmdecls.ML›
File ‹nominal_permeq.ML›
File ‹nominal_library.ML›
File ‹nominal_atoms.ML›
File ‹nominal_eqvt.ML›
HOL-Library.Quotient_Syntax
HOL-Library.Quotient_Set
HOL-Library.Quotient_Product
HOL-Library.Quotient_Option
HOL-Library.Quotient_List
Nominal2.Nominal2_Abs
Nominal2.Nominal2_FCB
Nominal2.Nominal2
File ‹nominal_dt_data.ML›
File ‹nominal_dt_rawfuns.ML›
File ‹nominal_dt_alpha.ML›
File ‹nominal_dt_quot.ML›
File ‹nominal_induct.ML›
File ‹nominal_inductive.ML›
File ‹nominal_function_common.ML›
File ‹nominal_function_core.ML›
File ‹nominal_mutual.ML›
File ‹nominal_function.ML›
File ‹nominal_termination.ML›
Pointwise
HOLCF-Utils
EvalHeap
Nominal-Utils
AList-Utils-Nominal
Nominal-HOLCF
Env-HOLCF
HasESem
Iterative
Env-Nominal
HeapSemantics
Vars
Terms
AbstractDenotational
Substitution
Abstract-Denotational-Props
Value
Value-Nominal
Denotational
Launchbury
CorrectnessOriginal
Mono-Nat-Fun
C
CValue
CValue-Nominal
HOLCF-Meet
C-Meet
C-restr
ResourcedDenotational
CorrectnessResourced
ResourcedAdequacy
ValueSimilarity
Denotational-Related
Adequacy
HOL-Library.LaTeXsugar
EverythingAdequacy