File OpmlPattern

File GenericModel

File OpmlSignature

File OpmlExamples

File KPreludeSignatures

File OpmlModel

File OpmlAmlRelSpec

File ProofSystemSoundness

File Freshness

File PrePredicate

File Signature

File ProofSystem

File stdpp_ext

File Lattice

File Surj

File extralibrary

• Module extralibrary: library functions, theorems, and tactics
  • Arithmetic
  • Peano induction.

File Unification

File ProofModePattern

File Nat_ProofSystem

File SumSort_ProofSystem

File Semantics

• • Matching Logic Semantics

File DerivedOperators_Syntax

File monotonic

File Firstorder

File Rewrite

File Complex

File tutorial

File Propositional

File Extractor

File Revert_size

File FreshnessManager

File ModelIsomorphism

File ApplicationContext

File IndexManipulation

File Syntax

File PatternContext

File Pattern

File FOEquality_ProofSystem

File Sorts_Semantics

File DefaultModels

File DeductionTheorem

File ContextualImplication

File ProductSort_ProofSystem

File Bool_Semantics

File RecursiveSymbol

File Definedness_ProofSystem

File Sorts_ProofSystem

File Bool_Syntax

File Definedness_Semantics

File Nat_Syntax

File ProductSortWithLookup

File ModelExtension

File Sorts_Syntax

File SumSort_Syntax

File ProductSort

File Bool_ProofSystem

File Subseteq_ProofSystem

File Definedness_Syntax

• Definedness

File wftactics

File Reshaper

File Firstorder

File FixPoint

File MLPM

File Propositional

File Misc

File Basics

File StringSignature

File NamedAxioms

File SyntacticConstruct

• General substitutions
• Substitution type classes for the different syntacical cateories

File Logic

File FreshnessApplicationCtx

File FreshnessSubstitution

File ApplicationCtxSubstitution

File PatternCtxApplicationCtx

File BasicProofSystemLemmas

File ProofInfo

File TEST_ProofMode_relative_completeness

File TEST_proofmode_example

File TEST_proofmode_proof_size

File TEST_LocallyNameless

File FixpointReasoning

File Substitution

File DerivedOperators_Semantics