Skip to content
[Jenkins]Jenkins
log in
Aborted

Changes

Summary

  1. clarified modules;
  2. clarified modules;
  3. discontinued obsolete "val extend = I" for data slots;
  4. clarified modules;
  5. clarified modules;
  6. clarified signature;
  7. tuned;
  8. clarified keywords and reports;
  9. clarified signature;
  10. merged
  11. proper veriT --max-time option
  12. refactored tptp_builtins in Sledgehammer
Changeset 74563:042041c0ebeb by wenzelm:
clarified modules;
The file was modified src/CCL/CCL.thy (diff)
The file was modified src/CCL/Wfd.thy (diff)
The file was modified src/CTT/CTT.thy (diff)
The file was modified src/Doc/Prog_Prove/LaTeXsugar.thy (diff)
The file was modified src/FOL/FOL.thy (diff)
The file was modified src/HOL/Eisbach/parse_tools.ML (diff)
The file was modified src/HOL/HOLCF/IOA/CompoScheds.thy (diff)
The file was modified src/HOL/HOLCF/IOA/Sequence.thy (diff)
The file was modified src/HOL/Library/LaTeXsugar.thy (diff)
The file was modified src/HOL/UNITY/UNITY_Main.thy (diff)
The file was modified src/LCF/LCF.thy (diff)
The file was modified src/Pure/Isar/args.ML (diff)
The file was modified src/Pure/Isar/locale.ML (diff)
The file was modified src/Pure/Isar/method.ML (diff)
The file was modified src/Pure/Isar/parse.ML (diff)
The file was modified src/Pure/ML/ml_antiquotation.ML (diff)
The file was modified src/Pure/ML/ml_antiquotations.ML (diff)
The file was modified src/Pure/ML/ml_thms.ML (diff)
The file was modified src/Pure/PIDE/resources.ML (diff)
The file was modified src/Pure/System/scala_compiler.ML (diff)
The file was modified src/Pure/Thy/document_antiquotations.ML (diff)
The file was modified src/Pure/Tools/jedit.ML (diff)
The file was modified src/Pure/Tools/named_theorems.ML (diff)
The file was modified src/Pure/Tools/plugin.ML (diff)
The file was modified src/Pure/Tools/rule_insts.ML (diff)
The file was modified src/Pure/simplifier.ML (diff)
The file was modified src/Tools/induct_tacs.ML (diff)
The file was modified src/ZF/Tools/ind_cases.ML (diff)
The file was modified src/ZF/Tools/induct_tacs.ML (diff)
The file was modified src/ZF/UNITY/SubstAx.thy (diff)
Changeset 74562:8403bd51f8b1 by wenzelm:
clarified modules;
The file was modified src/Pure/Isar/parse.ML (diff)
The file was modified src/Pure/Isar/token.ML (diff)
The file was modified src/Pure/ML/ml_antiquotations.ML (diff)
The file was modified src/Pure/ML/ml_context.ML (diff)
Changeset 74561:8e6c973003c8 by wenzelm:
discontinued obsolete "val extend = I" for data slots;
The file was modified NEWS (diff)
The file was modified src/Doc/Implementation/Prelim.thy (diff)
The file was modified src/HOL/Algebra/ringsimp.ML (diff)
The file was modified src/HOL/Analysis/measurable.ML (diff)
The file was modified src/HOL/Decision_Procs/Commutative_Ring.thy (diff)
The file was modified src/HOL/Decision_Procs/Reflective_Field.thy (diff)
The file was modified src/HOL/Decision_Procs/ferrante_rackoff_data.ML (diff)
The file was modified src/HOL/Decision_Procs/langford_data.ML (diff)
The file was modified src/HOL/Eisbach/Tests.thy (diff)
The file was modified src/HOL/Eisbach/method_closure.ML (diff)
The file was modified src/HOL/HOL.thy (diff)
The file was modified src/HOL/HOLCF/Tools/Domain/domain_take_proofs.ML (diff)
The file was modified src/HOL/HOLCF/Tools/fixrec.ML (diff)
The file was modified src/HOL/Hoare/hoare_syntax.ML (diff)
The file was modified src/HOL/Import/import_data.ML (diff)
The file was modified src/HOL/Library/adhoc_overloading.ML (diff)
The file was modified src/HOL/Library/code_lazy.ML (diff)
The file was modified src/HOL/Library/code_test.ML (diff)
The file was modified src/HOL/Library/datatype_records.ML (diff)
The file was modified src/HOL/Library/old_recdef.ML (diff)
The file was modified src/HOL/Library/refute.ML (diff)
The file was modified src/HOL/Nominal/nominal_atoms.ML (diff)
The file was modified src/HOL/Nominal/nominal_datatype.ML (diff)
The file was modified src/HOL/Nominal/nominal_thmdecls.ML (diff)
The file was modified src/HOL/Nonstandard_Analysis/transfer_principle.ML (diff)
The file was modified src/HOL/Real_Asymp/exp_log_expression.ML (diff)
The file was modified src/HOL/Real_Asymp/multiseries_expansion.ML (diff)
The file was modified src/HOL/SPARK/Tools/spark_vcs.ML (diff)
The file was modified src/HOL/Statespace/state_fun.ML (diff)
The file was modified src/HOL/Statespace/state_space.ML (diff)
The file was modified src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML (diff)
The file was modified src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML (diff)
The file was modified src/HOL/Tools/Argo/argo_tactic.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_def.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_grec.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_lfp_size.ML (diff)
The file was modified src/HOL/Tools/Ctr_Sugar/case_translation.ML (diff)
The file was modified src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML (diff)
The file was modified src/HOL/Tools/Function/function_common.ML (diff)
The file was modified src/HOL/Tools/Function/function_context_tree.ML (diff)
The file was modified src/HOL/Tools/Function/partial_function.ML (diff)
The file was modified src/HOL/Tools/Function/scnp_reconstruct.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_def.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_def_code_dt.ML (diff)
The file was modified src/HOL/Tools/Lifting/lifting_info.ML (diff)
The file was modified src/HOL/Tools/Nitpick/nitpick_commands.ML (diff)
The file was modified src/HOL/Tools/Nitpick/nitpick_hol.ML (diff)
The file was modified src/HOL/Tools/Nitpick/nitpick_model.ML (diff)
The file was modified src/HOL/Tools/Nunchaku/nunchaku_commands.ML (diff)
The file was modified src/HOL/Tools/Old_Datatype/old_datatype_data.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_data.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML (diff)
The file was modified src/HOL/Tools/Predicate_Compile/predicate_compile_specialisation.ML (diff)
The file was modified src/HOL/Tools/Qelim/cooper.ML (diff)
The file was modified src/HOL/Tools/Quickcheck/quickcheck_common.ML (diff)
The file was modified src/HOL/Tools/Quotient/quotient_info.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_builtin.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_config.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_normalize.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_replay.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_replay_methods.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_solver.ML (diff)
The file was modified src/HOL/Tools/SMT/smt_translate.ML (diff)
The file was modified src/HOL/Tools/SMT/smtlib_interface.ML (diff)
The file was modified src/HOL/Tools/SMT/smtlib_proof.ML (diff)
The file was modified src/HOL/Tools/SMT/verit_proof.ML (diff)
The file was modified src/HOL/Tools/SMT/z3_interface.ML (diff)
The file was modified src/HOL/Tools/SMT/z3_replay_rules.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML (diff)
The file was modified src/HOL/Tools/Transfer/transfer.ML (diff)
The file was modified src/HOL/Tools/arith_data.ML (diff)
The file was modified src/HOL/Tools/functor.ML (diff)
The file was modified src/HOL/Tools/inductive.ML (diff)
The file was modified src/HOL/Tools/inductive_set.ML (diff)
The file was modified src/HOL/Tools/lin_arith.ML (diff)
The file was modified src/HOL/Tools/record.ML (diff)
The file was modified src/HOL/Tools/reflection.ML (diff)
The file was modified src/HOL/Tools/semiring_normalizer.ML (diff)
The file was modified src/HOL/Tools/typedef.ML (diff)
The file was modified src/HOL/Tools/value_command.ML (diff)
The file was modified src/Provers/Arith/fast_lin_arith.ML (diff)
The file was modified src/Provers/classical.ML (diff)
The file was modified src/Provers/order_tac.ML (diff)
The file was modified src/Pure/Concurrent/thread_data_virtual.ML (diff)
The file was modified src/Pure/General/name_space.ML (diff)
The file was modified src/Pure/Isar/attrib.ML (diff)
The file was modified src/Pure/Isar/bundle.ML (diff)
The file was modified src/Pure/Isar/calculation.ML (diff)
The file was modified src/Pure/Isar/class.ML (diff)
The file was modified src/Pure/Isar/code.ML (diff)
The file was modified src/Pure/Isar/context_rules.ML (diff)
The file was modified src/Pure/Isar/experiment.ML (diff)
The file was modified src/Pure/Isar/generic_target.ML (diff)
The file was modified src/Pure/Isar/local_defs.ML (diff)
The file was modified src/Pure/Isar/locale.ML (diff)
The file was modified src/Pure/Isar/method.ML (diff)
The file was modified src/Pure/Isar/object_logic.ML (diff)
The file was modified src/Pure/Isar/outer_syntax.ML (diff)
The file was modified src/Pure/Isar/spec_rules.ML (diff)
The file was modified src/Pure/ML/ml_context.ML (diff)
The file was modified src/Pure/ML/ml_env.ML (diff)
The file was modified src/Pure/ML/ml_thms.ML (diff)
The file was modified src/Pure/PIDE/resources.ML (diff)
The file was modified src/Pure/Proof/extraction.ML (diff)
The file was modified src/Pure/Syntax/syntax.ML (diff)
The file was modified src/Pure/Syntax/syntax_phases.ML (diff)
The file was modified src/Pure/Thy/document_antiquotation.ML (diff)
The file was modified src/Pure/Thy/document_marker.ML (diff)
The file was modified src/Pure/Thy/export_theory.ML (diff)
The file was modified src/Pure/Thy/term_style.ML (diff)
The file was modified src/Pure/Thy/thy_header.ML (diff)
The file was modified src/Pure/Thy/thy_info.ML (diff)
The file was modified src/Pure/Tools/generated_files.ML (diff)
The file was modified src/Pure/Tools/named_theorems.ML (diff)
The file was modified src/Pure/Tools/named_thms.ML (diff)
The file was modified src/Pure/Tools/plugin.ML (diff)
The file was modified src/Pure/Tools/simplifier_trace.ML (diff)
The file was modified src/Pure/axclass.ML (diff)
The file was modified src/Pure/config.ML (diff)
The file was modified src/Pure/context.ML (diff)
The file was modified src/Pure/ex/Def.thy (diff)
The file was modified src/Pure/global_theory.ML (diff)
The file was modified src/Pure/more_thm.ML (diff)
The file was modified src/Pure/proofterm.ML (diff)
The file was modified src/Pure/pure_thy.ML (diff)
The file was modified src/Pure/raw_simplifier.ML (diff)
The file was modified src/Pure/sign.ML (diff)
The file was modified src/Pure/simplifier.ML (diff)
The file was modified src/Pure/soft_type_system.ML (diff)
The file was modified src/Pure/theory.ML (diff)
The file was modified src/Pure/thm.ML (diff)
The file was modified src/Sequents/prover.ML (diff)
The file was modified src/Tools/Code/code_preproc.ML (diff)
The file was modified src/Tools/Code/code_runtime.ML (diff)
The file was modified src/Tools/Code/code_simp.ML (diff)
The file was modified src/Tools/Code/code_target.ML (diff)
The file was modified src/Tools/induct.ML (diff)
The file was modified src/Tools/nbe.ML (diff)
The file was modified src/Tools/quickcheck.ML (diff)
The file was modified src/Tools/subtyping.ML (diff)
The file was modified src/Tools/try.ML (diff)
The file was modified src/ZF/Tools/ind_cases.ML (diff)
The file was modified src/ZF/Tools/induct_tacs.ML (diff)
The file was modified src/ZF/Tools/typechk.ML (diff)
Changeset 74560:5c8177fd1295 by wenzelm:
clarified modules;
The file was modified src/HOL/Real_Asymp/real_asymp.ML (diff)
The file was modified src/Pure/conv.ML (diff)
Changeset 74559:9189d949abb9 by wenzelm:
clarified modules;
The file was addedsrc/Pure/ML/ml_antiquotations.ML
The file was modified src/Pure/Isar/locale.ML (diff)
The file was modified src/Pure/Isar/method.ML (diff)
The file was modified src/Pure/ROOT.ML (diff)
The file was removedsrc/Pure/ML/ml_antiquotations1.ML
The file was removedsrc/Pure/ML/ml_antiquotations2.ML
Changeset 74558:44dc1661a5cb by wenzelm:
clarified signature;
The file was modified src/HOL/Tools/Mirabelle/mirabelle.ML (diff)
The file was modified src/Pure/Isar/method.ML (diff)
The file was modified src/Pure/Isar/token.ML (diff)
The file was modified src/Pure/Thy/document_marker.ML (diff)
Changeset 74557:59febd85a0f6 by wenzelm:
tuned;
The file was modified src/Pure/Thy/document_antiquotation.ML (diff)
Changeset 74556:b45b85a4145e by wenzelm:
clarified keywords and reports;
The file was modified src/Pure/ML/ml_antiquotations1.ML (diff)
Changeset 74555:3ba399ecdfaf by wenzelm:
clarified signature;
The file was modified src/Pure/Isar/keyword.ML (diff)
The file was modified src/Pure/Tools/find_consts.ML (diff)
The file was modified src/Pure/Tools/find_theorems.ML (diff)
Changeset 74554:67c4004495f2 by desharna:
merged
Changeset 74553:3ec9cafab990 by desharna:
proper veriT --max-time option
The file was modified src/HOL/Tools/SMT/smt_systems.ML (diff)
Changeset 74552:f55c632a1fe8 by desharna:
refactored tptp_builtins in Sledgehammer
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)