Summary
- towards support for HO SMT-LIB
- Some small lemmas about polynomials and FPSs
- tuned names
The file was modified | src/HOL/SMT.thy (diff) |
The file was modified | src/HOL/Tools/SMT/cvc4_interface.ML (diff) |
The file was modified | src/HOL/Tools/SMT/smt_builtin.ML (diff) |
The file was modified | src/HOL/Tools/SMT/smt_config.ML (diff) |
The file was modified | src/HOL/Tools/SMT/smt_real.ML (diff) |
The file was modified | src/HOL/Tools/SMT/smt_systems.ML (diff) |
The file was modified | src/HOL/Tools/SMT/smt_translate.ML (diff) |
The file was modified | src/HOL/Tools/SMT/smt_util.ML (diff) |
The file was modified | src/HOL/Tools/SMT/smtlib_interface.ML (diff) |
The file was modified | src/HOL/Tools/SMT/z3_interface.ML (diff) |
The file was modified | src/HOL/Word/Tools/smt_word.ML (diff) |
The file was modified | src/HOL/Computational_Algebra/Formal_Power_Series.thy (diff) |
The file was modified | src/HOL/Computational_Algebra/Polynomial.thy (diff) |
The file was modified | src/HOL/List.thy (diff) |
The file was modified | src/HOL/Data_Structures/Binomial_Heap.thy (diff) |