Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. uniform use of Standard ML op-infix -- eliminated warnings;
  2. proper infix;
  3. line break before op was intentional
Changeset 67405:e9ab4ad7bd15 by wenzelm:
uniform use of Standard ML op-infix -- eliminated warnings;
The file was modified src/CTT/CTT.thy (diff)
The file was modified src/FOLP/IFOLP.thy (diff)
The file was modified src/HOL/Bali/AxExample.thy (diff)
The file was modified src/HOL/HOL.thy (diff)
The file was modified src/HOL/Library/Countable.thy (diff)
The file was modified src/HOL/Library/Pattern_Aliases.thy (diff)
The file was modified src/HOL/Library/refute.ML (diff)
The file was modified src/HOL/Matrix_LP/Cplex_tools.ML (diff)
The file was modified src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML (diff)
The file was modified src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML (diff)
The file was modified src/HOL/Nitpick_Examples/Mono_Nits.thy (diff)
The file was modified src/HOL/Nominal/nominal_datatype.ML (diff)
The file was modified src/HOL/Nominal/nominal_inductive.ML (diff)
The file was modified src/HOL/Nominal/nominal_inductive2.ML (diff)
The file was modified src/HOL/Orderings.thy (diff)
The file was modified src/HOL/Proofs/ex/Proof_Terms.thy (diff)
The file was modified src/HOL/SMT_Examples/boogie.ML (diff)
The file was modified src/HOL/TPTP/TPTP_Proof_Reconstruction.thy (diff)
The file was modified src/HOL/Tools/ATP/atp_problem.ML (diff)
The file was modified src/HOL/Tools/ATP/atp_problem_generate.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp.ML (diff)
The file was modified src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML (diff)
The file was modified src/HOL/Tools/Nitpick/nitpick_commands.ML (diff)
The file was modified src/HOL/Tools/Nitpick/nitpick_mono.ML (diff)
The file was modified src/HOL/Tools/Nunchaku/nunchaku_collect.ML (diff)
The file was modified src/HOL/Tools/Nunchaku/nunchaku_commands.ML (diff)
The file was modified src/HOL/Tools/Nunchaku/nunchaku_reconstruct.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/code_prolog.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/core_data.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML (diff)
The file was modified src/HOL/Tools/Qelim/cooper.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_systems.ML (diff)
The file was modified src/HOL/Tools/SMT/smtlib.ML (diff)
The file was modified src/HOL/Tools/SMT/smtlib_interface.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_isar_proof.ML (diff)
The file was modified src/HOL/Tools/datatype_realizer.ML (diff)
The file was modified src/HOL/Tools/functor.ML (diff)
The file was modified src/HOL/Tools/groebner.ML (diff)
The file was modified src/HOL/Tools/sat_solver.ML (diff)
The file was modified src/HOL/Word/WordBitwise.thy (diff)
Changeset 67404:e128ab544996 by wenzelm:
proper infix;
The file was modified src/HOL/TPTP/TPTP_Proof_Reconstruction.thy (diff)
Changeset 67403:90fe8c635ba0 by nipkow:
line break before op was intentional
The file was modified src/HOL/Orderings.thy (diff)
The file was modified src/HOL/Set.thy (diff)