Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. added 'mlex_iff' lemma and simplified proof
  2. merged
  3. recovered document from 9bfb6978eb80;
  4. NEWS;
  5. obsolete;
  6. tuned;
  7. ROOT cleanup: empty 'document_files' means there is no document;
  8. eliminated pointless warning (see a35af478aee4): empty 'document_files' means there is no document;
  9. more informative timeout message, notably for build_status;
  10. clarified: adapted to ML version;
  11. proper order of initialization (amending 9953ae603a23);
  12. More topological results overlooked last time
  13. merged
  14. New results in topology, mostly from HOL Light's moretop.ml
  15. generalized some lemmas on multisets
  16. rule out pathologic instances
  17. tuned some proofs and added some lemmas
Changeset 66952:80985b62029d by blanchet:
added 'mlex_iff' lemma and simplified proof
The file was modified src/HOL/Wellfounded.thy (diff)
Changeset 66951:dd4710b91277 by wenzelm:
merged
Changeset 66950:1a5e90026391 by wenzelm:
recovered document from 9bfb6978eb80;
The file was modified src/HOL/ROOT (diff)
Changeset 66949:6c5e4ac0398b by wenzelm:
NEWS;
The file was modified NEWS (diff)
Changeset 66948:47249c5ec3a4 by wenzelm:
obsolete;
The file was modified lib/Tools/mkroot (diff)
Changeset 66947:eefbb2300669 by wenzelm:
tuned;
The file was modified src/Doc/System/Environment.thy (diff)
Changeset 66946:3d8fd98c7c86 by wenzelm:
ROOT cleanup: empty 'document_files' means there is no document;
The file was modified src/Benchmarks/ROOT (diff)
The file was modified src/CCL/ROOT (diff)
The file was modified src/Cube/ROOT (diff)
The file was modified src/Doc/ROOT (diff)
The file was modified src/FOLP/ROOT (diff)
The file was modified src/HOL/ROOT (diff)
The file was modified src/LCF/ROOT (diff)
The file was modified src/Sequents/ROOT (diff)
The file was modified src/ZF/ROOT (diff)
Changeset 66945:b6f787a17fbe by wenzelm:
eliminated pointless warning (see a35af478aee4): empty 'document_files' means there is no document;
The file was modified src/Pure/Thy/present.ML (diff)
Changeset 66944:05df740cb54b by wenzelm:
more informative timeout message, notably for build_status;
The file was modified src/Pure/Admin/build_log.scala (diff)
The file was modified src/Pure/Tools/build.scala (diff)
Changeset 66943:351aaaa9bacd by wenzelm:
clarified: adapted to ML version;
The file was modified src/Pure/Tools/build.scala (diff)
Changeset 66942:91a21a5631ae by wenzelm:
proper order of initialization (amending 9953ae603a23);
The file was modified src/Pure/PIDE/markup.scala (diff)
Changeset 66941:c67bb79a0ceb by paulson _lp15@cam.ac.uk_:
More topological results overlooked last time
The file was modified src/HOL/Analysis/Further_Topology.thy (diff)
The file was modified src/HOL/Analysis/Riemann_Mapping.thy (diff)
Changeset 66940:e5776e8e152b by paulson:
merged
Changeset 66939:04678058308f by paulson _lp15@cam.ac.uk_:
New results in topology, mostly from HOL Light's moretop.ml
The file was modified src/HOL/Analysis/Brouwer_Fixpoint.thy (diff)
The file was modified src/HOL/Analysis/Connected.thy (diff)
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
The file was modified src/HOL/Analysis/Further_Topology.thy (diff)
The file was modified src/HOL/Analysis/Path_Connected.thy (diff)
The file was modified src/HOL/Analysis/Topology_Euclidean_Space.thy (diff)
Changeset 66938:c78ff0aeba4c by haftmann:
generalized some lemmas on multisets
The file was modified src/HOL/Computational_Algebra/Factorial_Ring.thy (diff)
The file was modified src/HOL/Library/Multiset.thy (diff)
Changeset 66937:a1a4a5e2933a by haftmann:
rule out pathologic instances
The file was modified NEWS (diff)
The file was modified src/HOL/Rings.thy (diff)
Changeset 66936:cf8d8fc23891 by haftmann:
tuned some proofs and added some lemmas
The file was modified src/HOL/Analysis/Gamma_Function.thy (diff)
The file was modified src/HOL/GCD.thy (diff)
The file was modified src/HOL/Groups_Big.thy (diff)
The file was modified src/HOL/Inequalities.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)
The file was modified src/HOL/Library/Numeral_Type.thy (diff)
The file was modified src/HOL/Library/Uprod.thy (diff)
The file was modified src/HOL/Nat.thy (diff)
The file was modified src/HOL/Num.thy (diff)
The file was modified src/HOL/Orderings.thy (diff)
The file was modified src/HOL/Power.thy (diff)
The file was modified src/HOL/Set_Interval.thy (diff)
The file was modified src/HOL/ex/Function_Growth.thy (diff)