Skip to content
Success

Changes

Summary

  1. merged
  2. proper constants in TPTP $let binding
  3. more operations from Isabelle/ML;
  4. merged
  5. tuned proofs --- eliminated 'guess';
  6. tuned proofs; tuned whitespace;
  7. clarified antiquotations;
  8. proper firstorderization in Sledgehammer
Changeset 74329:949054d78a77 by desharna:
merged
Changeset 74328:404ce20efc4c by desharna:
proper constants in TPTP $let binding
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)
Changeset 74327:9dca3df78b6a by wenzelm:
more operations from Isabelle/ML;
The file was modified src/Tools/Haskell/Haskell.thy (diff)
Changeset 74326:b8a191ce08aa by wenzelm:
merged
Changeset 74325:8d0c2d74ad63 by wenzelm:
tuned proofs --- eliminated 'guess';
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)
Changeset 74324:308e74afab83 by wenzelm:
tuned proofs;<br>tuned whitespace;
The file was modified src/HOL/Library/Landau_Symbols.thy (diff)
Changeset 74323:5c452041fe83 by wenzelm:
clarified antiquotations;
The file was modified src/HOL/Tools/Argo/argo_real.ML (diff)
The file was modified src/HOL/Tools/Argo/argo_tactic.ML (diff)
Changeset 74322:102b55e81aca by desharna:
proper firstorderization in Sledgehammer
The file was modified src/HOL/Tools/ATP/atp_problem_generate.ML (diff)