Session Applicative_Lifting

Theories

• Applicative
  • File ‹applicative.ML›
• Applicative_Environment
• Applicative_Option
• Applicative_Sum
• Applicative_Set
• Applicative_List
• HOL-Library.Confluence
• HOL-Library.Confluent_Quotient
• HOL-Library.Dlist
• Applicative_DNEList
• Applicative_Monoid
• Applicative_Filter
• HOL-Library.State_Monad
• Applicative_State
• Applicative_Stream
• Applicative_Open_State
• Applicative_PMF
• Applicative_Probability_List
• HOL-Nonstandard_Analysis.Free_Ultrafilter
• HOL-Nonstandard_Analysis.StarDef
  • File ‹transfer_principle.ML›
• Applicative_Star
• Applicative_Vector
• Applicative_Functor
• HOL-Library.Function_Algebras
• HOL-Library.Function_Division
• Applicative_Environment_Algebra
• Stream_Algebra
• Tree_Relabelling
• Applicative_Examples
• HOL-Proofs-Lambda.Lambda
• HOL-Proofs-Lambda.Commutation
• HOL-Proofs-Lambda.ParRed
• HOL-Proofs-Lambda.Eta
• Joinable
• Beta_Eta
• Combinators
• Idiomatic_Terms
• Abstract_AF
• Applicative_Test