Package function-def-comb: function-def-comb

Information

Files

• Package tarball function-def-comb-1.0.tgz
• Theory file function-def-comb.thy (included in the package tarball)

Defined Constants

• Function
  • Function.id
  • Function.o

Theorems

⊦ Function.id = λx. x

⊦ ∀f g. Function.o f g = λx. f (g x)

Input Type Operators

• →
• bool

Input Constants

• =
• Data
  • Bool
    • ∀
    • T

Assumptions

⊦ T

⊦ (∀) = λP. P = λx. T