Session CDCL

Theories

• HOL-Eisbach.Eisbach
  • File ‹parse_tools.ML›
  • File ‹method_closure.ML›
  • File ‹eisbach_rule_insts.ML›
  • File ‹match_method.ML›
• HOL-Eisbach.Eisbach_Tools
• HOL-Library.Old_Datatype
  • File ‹~~/src/HOL/Tools/Old_Datatype/old_datatype.ML›
• HOL-Library.Nat_Bijection
• HOL-Library.Countable
  • File ‹~~/src/HOL/Tools/BNF/bnf_lfp_countable.ML›
• HOL-Library.FSet
• HOL-Library.AList
• HOL-Library.Conditional_Parametricity
  • File ‹conditional_parametricity.ML›
• HOL-Library.Finite_Map
• 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.Multiset_Order
• HOL-Library.Sublist
• Nested_Multisets_Ordinals.Multiset_More
• Nested_Multisets_Ordinals.Duplicate_Free_Multiset
• HOL-Library.FuncSet
• Weidenbach_Book_Base.WB_List_More
• Ordered_Resolution_Prover.Clausal_Logic
• Entailment_Definition.Partial_Herbrand_Interpretation
• Entailment_Definition.Partial_Annotated_Herbrand_Interpretation
• Weidenbach_Book_Base.Wellfounded_More
• DPLL_W
• CDCL_W_Level
• CDCL_W
• CDCL_W_Termination
• CDCL_W_Merge
• CDCL_WNOT_Measure
• CDCL_NOT
• CDCL_WNOT
• CDCL_W_Full
• CDCL_W_Restart
• CDCL_W_Incremental
• DPLL_CDCL_W_Implementation
• HOL-Library.Code_Target_Int
• HOL-Library.Code_Abstract_Nat
• HOL-Library.Code_Target_Nat
• HOL-Library.Code_Target_Numeral
• DPLL_W_Implementation
• CDCL_W_Implementation
• CDCL_Abstract_Clause_Representation
• CDCL_W_Abstract_State
• Pragmatic_CDCL
• Pragmatic_CDCL_Restart