Changes

Summary

more on Isabelle_System.bash;
more specific name
more lemmas
dropped obscure FIXME
proper usage of hypotheses for zipperposition's TPTP generation
merged
tuned Mirabelle to parse option check_trivial only once
merged
merged
added stride option to Mirabelle
proper prover capabilities for zipperposition

Changeset 73298:637e3e85cd6f by wenzelm: more on Isabelle_System.bash;
The file was modified	`NEWS` (diff)
Changeset 73297:beaff25452d2 by haftmann: more specific name
The file was added	`src/HOL/Library/List_Permutation.thy`
The file was modified	`NEWS` (diff)
The file was modified	`src/HOL/Algebra/Divisibility.thy` (diff)
The file was modified	`src/HOL/Library/Library.thy` (diff)
The file was modified	`src/HOL/Probability/ex/Koepf_Duermuth_Countermeasure.thy` (diff)
The file was removed	`src/HOL/Library/Permutation.thy`
Changeset 73296:2ac92ba88d6b by haftmann: more lemmas
The file was modified	`src/HOL/Library/Function_Algebras.thy` (diff)
Changeset 73295:6c4c37a3ebec by haftmann: dropped obscure FIXME
The file was modified	`src/HOL/Lattices_Big.thy` (diff)
Changeset 73294:f0210642e43f by desharna: proper usage of hypotheses for zipperposition's TPTP generation
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML` (diff)
Changeset 73293:8b6fa865bac4 by desharna: merged
Changeset 73292:f84a93f1de2f by desharna: tuned Mirabelle to parse option check_trivial only once
The file was modified	`src/HOL/Mirabelle/Tools/mirabelle.ML` (diff)
The file was modified	`src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML` (diff)
Changeset 73291:efeebcfaef85 by desharna: merged
Changeset 73290:dcf295994c90 by desharna: merged
Changeset 73289:a34b49841585 by desharna: added stride option to Mirabelle
The file was modified	`src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML` (diff)
Changeset 73288:f6f1242ed367 by desharna: proper prover capabilities for zipperposition
The file was modified	`src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML` (diff)