Session Simplicial_complexes_and_boolean_functions

Theories

• HOL-Computational_Algebra.Factorial_Ring
• Polynomial_Interpolation.Ring_Hom
• HOL-Library.FuncSet
• HOL-Library.Disjoint_Sets
• HOL-Combinatorics.Transposition
• HOL-Combinatorics.Permutations
• Jordan_Normal_Form.Missing_Misc
• HOL-Algebra.Congruence
• HOL-Algebra.Order
• HOL-Algebra.Lattice
• HOL-Algebra.Complete_Lattice
• HOL-Algebra.Group
• HOL-Algebra.FiniteProduct
• HOL-Algebra.Ring
  • File ‹ringsimp.ML›
• Jordan_Normal_Form.Missing_Ring
• HOL-Library.Complex_Order
• Jordan_Normal_Form.Conjugate
• HOL-Algebra.Module
• Jordan_Normal_Form.Matrix
• Boolean_functions
• Simplicial_complex
• Bij_betw_simplicial_complex_bool_func
• ROBDD.Bool_Func
• ROBDD.BDT
• MkIfex
• Evasive
• ROBDD.Array_List
• ROBDD.Pointer_Map
• ROBDD.Pointer_Map_Impl
• ROBDD.Option_Helpers
• ROBDD.Abstract_Impl
• ROBDD.Middle_Impl
• ROBDD.Conc_Impl
• ROBDD.Level_Collapse
• ListLexorder
• BDD
• Binary_operations