Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. eliminated one redundant proof obligation in lift_bnf for quotients
  3. removed experimental option to SPASS
  4. alternative deletion in Red-Black trees
  5. generalized thm (as suggested by Christian Weinz)
  6. tunded
Changeset 71355:15c6f253b9f3 by traytel:
merged
Changeset 71354:c71a44893645 by traytel:
eliminated one redundant proof obligation in lift_bnf for quotients
The file was modified src/Doc/Datatypes/Datatypes.thy (diff)
The file was modified src/HOL/Datatype_Examples/TLList.thy (diff)
The file was modified src/HOL/Quotient.thy (diff)
The file was modified src/HOL/Tools/BNF/bnf_lift.ML (diff)
Changeset 71353:475b2260b9c4 by blanchet:
removed experimental option to SPASS
The file was modified src/HOL/Tools/ATP/atp_systems.ML (diff)
Changeset 71352:41f3ca717da5 by nipkow:
alternative deletion in Red-Black trees
The file was addedsrc/HOL/Data_Structures/RBT_Set2.thy
The file was modified src/HOL/Data_Structures/document/root.tex (diff)
The file was modified src/HOL/ROOT (diff)
Changeset 71351:b3a93a91803b by nipkow:
generalized thm (as suggested by Christian Weinz)
The file was modified src/HOL/Binomial.thy (diff)
Changeset 71350:cd0b0717c4e4 by nipkow:
tunded
The file was modified src/HOL/Data_Structures/RBT_Set.thy (diff)