Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
  3. tuned code setup
  4. strengthened tactic
  5. Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
  6. strengthened tactic (for 'fun' BNF)
Changeset 66293:2eae295c8fc3 by lars hupel _lars.hupel@mytum.de_:
merged
Changeset 66292:9930f4cf6c7a by lars hupel _lars.hupel@mytum.de_:
improve setup for fMin/fMax/fsum; courtesy of Ondřej Kunčar & Florian Haftmann
The file was modified src/HOL/Library/FSet.thy (diff)
Changeset 66291:f32968e099d5 by lars hupel _lars.hupel@mytum.de_:
tuned code setup
The file was modified src/HOL/Library/Finite_Map.thy (diff)
Changeset 66290:88714f2e40e8 by blanchet:
strengthened tactic
The file was modified src/HOL/BNF_Least_Fixpoint.thy (diff)
The file was modified src/HOL/Nat.thy (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_rec_sugar_more.ML (diff)
Changeset 66289:2562f151541c by paulson _lp15@cam.ac.uk_:
Divided Convex_Euclidean_Space.thy in half, creating new theory Starlike
The file was addedsrc/HOL/Analysis/Starlike.thy
The file was modified src/HOL/Analysis/Continuous_Extension.thy (diff)
The file was modified src/HOL/Analysis/Convex_Euclidean_Space.thy (diff)
Changeset 66288:e5995950b98a by blanchet:
strengthened tactic (for 'fun' BNF)
The file was modified src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML (diff)