Summary
- merged
- split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
- proper name mangling of "undefined" constants in Sledgehammer
- earlier availability of lifting
- more correct transfer
- merged
- proper abstraction of function variables when instantiating induction rules in Sledgehammer
- added lemma asympD
- added lemma
- Some lemmas about continuous functions with integral zero
The file was modified | NEWS |
The file was modified | src/Doc/Sledgehammer/document/root.tex |
The file was modified | src/HOL/TPTP/mash_eval.ML |
The file was modified | src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML |
The file was modified | src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML |
The file was modified | src/HOL/Tools/ATP/atp_problem_generate.ML |
The file was modified | src/HOL/Equiv_Relations.thy |
The file was modified | src/HOL/Groups_Big.thy |
The file was modified | src/HOL/Int.thy |
The file was modified | src/HOL/Lattices_Big.thy |
The file was modified | src/HOL/Lifting_Set.thy |
The file was modified | src/Pure/Isar/code.ML |
The file was modified | src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML |
The file was modified | src/HOL/Relation.thy |
The file was modified | src/HOL/Library/While_Combinator.thy |
The file was modified | src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy |
Summary
- Tuning.
- merged
- tweaks
- merged
- Fixed an inadequate description
- tuned
- mv to distribution
- by now in distribution
- merge from afp-2021-1
- fixed abstract
- tuned
- website and metadata for Hyperdual
- new entry: Hyperdual
- sorted ROOTS
- tuned
- New entry Knights_Tour
- more thoroughly replace Michael Foster's e-mail address
- metadata and sitegen for Gale_Shapley
- new entry Gale_Shapley
- update Michael Forster's email address
- metadata and sitegen for Roth_Arithmetic_Progressions
- new entry Roth_Arithmetic_Progressions
- typo
- merged
- New entry Regular_Tree_Relations
- We DON'T want an output directory
- MDP-Algorithms website
- new entry MDP-Algorithms
- typo
- new entry MDP-Rewards
- fixed typo