Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. merged
  2. more informative Spec_Rules.Equational, notably primrec argument types;
  3. clarified signature: avoid direct comparison on type rough_classification;
  4. tuned proofs;
  5. removed spurious debugging;
  6. export propositional status of consts;
  7. merged
  8. generalised homotopic_with to topologies; homotopic_with_canon is the old version
  9. follow up on Braun: get timing function right
  10. Tweak Braun tree list_fast_rec recursion. A minor adjustment simplifies the termination argument slightly.
Changeset 69993:3fd083253a1c by wenzelm:
merged
Changeset 69992:bd3c10813cc4 by wenzelm:
more informative Spec_Rules.Equational, notably primrec argument types;
The file was modified src/HOL/Library/old_recdef.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_gfp_grec_sugar.ML (diff)
The file was modified src/HOL/Tools/BNF/bnf_gfp_rec_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/ctr_sugar.ML (diff)
The file was modified src/HOL/Tools/Function/function.ML (diff)
The file was modified src/HOL/Tools/Function/partial_function.ML (diff)
The file was modified src/HOL/Tools/Nunchaku/nunchaku_collect.ML (diff)
The file was modified src/HOL/Tools/Old_Datatype/old_primrec.ML (diff)
The file was modified src/HOL/Tools/record.ML (diff)
The file was modified src/Pure/Isar/spec_rules.ML (diff)
The file was modified src/Pure/Isar/specification.ML (diff)
The file was modified src/Pure/Proof/extraction.ML (diff)
The file was modified src/Pure/Thy/export_theory.ML (diff)
The file was modified src/Pure/Thy/export_theory.scala (diff)
Changeset 69991:6b097aeb3650 by wenzelm:
clarified signature: avoid direct comparison on type rough_classification;
The file was modified src/HOL/Tools/Nitpick/nitpick_hol.ML (diff)
The file was modified src/HOL/Tools/Nunchaku/nunchaku_collect.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML (diff)
The file was modified src/Pure/Isar/spec_rules.ML (diff)
Changeset 69990:eb072ce80f82 by wenzelm:
tuned proofs;
The file was modified src/HOL/Quotient.thy (diff)
Changeset 69989:bcba61d92558 by wenzelm:
removed spurious debugging;
The file was modified src/HOL/Metis_Examples/Type_Encodings.thy (diff)
The file was modified src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy (diff)
Changeset 69988:6fa51a36b7f7 by wenzelm:
export propositional status of consts;
The file was modified src/Pure/Isar/object_logic.ML (diff)
The file was modified src/Pure/Thy/export_theory.ML (diff)
The file was modified src/Pure/Thy/export_theory.scala (diff)
Changeset 69987:e7648f104d6b by paulson:
merged
Changeset 69986:f2d327275065 by paulson _lp15@cam.ac.uk_:
generalised homotopic_with to topologies; homotopic_with_canon is the old version
The file was modified src/HOL/Analysis/Abstract_Topology.thy (diff)
The file was modified src/HOL/Analysis/Brouwer_Fixpoint.thy (diff)
The file was modified src/HOL/Analysis/Complex_Transcendental.thy (diff)
The file was modified src/HOL/Analysis/Further_Topology.thy (diff)
The file was modified src/HOL/Analysis/Homeomorphism.thy (diff)
The file was modified src/HOL/Analysis/Homotopy.thy (diff)
The file was modified src/HOL/Analysis/Jordan_Curve.thy (diff)
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Analysis/Product_Topology.thy (diff)
The file was modified src/HOL/Analysis/T1_Spaces.thy (diff)
The file was modified src/HOL/Analysis/Winding_Numbers.thy (diff)
The file was modified src/HOL/Complete_Lattices.thy (diff)
The file was modified src/HOL/Set.thy (diff)
Changeset 69985:8e916ed23d17 by thomas sewell _sewell@chalmers.se_:
follow up on Braun: get timing function right
The file was modified src/HOL/Data_Structures/Array_Braun.thy (diff)
Changeset 69984:3afa3b25b5e7 by thomas sewell _sewell@chalmers.se_:
Tweak Braun tree list_fast_rec recursion.<br><br>A minor adjustment simplifies the termination argument slightly.
The file was modified src/HOL/Data_Structures/Array_Braun.thy (diff)