Summary
- merged
- proper constants in TPTP $let binding
- more operations from Isabelle/ML;
- merged
- tuned proofs --- eliminated 'guess';
- tuned proofs; tuned whitespace;
- clarified antiquotations;
- proper firstorderization in Sledgehammer
The file was modified | src/HOL/Tools/ATP/atp_problem_generate.ML (diff) |
The file was modified | src/HOL/Tools/ATP/atp_util.ML (diff) |
The file was modified | src/Tools/Haskell/Haskell.thy (diff) |
The file was modified | src/HOL/Filter.thy (diff) |
The file was modified | src/HOL/Library/Countable_Set.thy (diff) |
The file was modified | src/HOL/Library/Extended_Nonnegative_Real.thy (diff) |
The file was modified | src/HOL/Library/Extended_Real.thy (diff) |
The file was modified | src/HOL/Library/Landau_Symbols.thy (diff) |
The file was modified | src/HOL/Tools/Argo/argo_real.ML (diff) |
The file was modified | src/HOL/Tools/Argo/argo_tactic.ML (diff) |
The file was modified | src/HOL/Tools/ATP/atp_problem_generate.ML (diff) |