Skip to content
Success

Changes

Summary

  1. merged
  2. Hiding the constant "norm", lest it clash with the norm of a vector space
  3. more lemmas from Paulo
  4. merged
  5. updated for release;
  6. Added tag Isabelle2018-RC1 for changeset cf01d04e94d7
  7. fixed (?) LaTeX presentation
  8. merged
  9. Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
  10. more NEWS;
  11. tuned;
  12. more robust: avoid dire effect of ui.tweakoptions on hg.known_files;
  13. update Sledgehammer docs w.r.t. Vampire
  14. added Vampire component
  15. added option for noncommercial Vampire
Changeset 68577:c0b978f6ecd1 by paulson:
merged
Changeset 68576:b6cc5c265b04 by paulson _lp15@cam.ac.uk_:
Hiding the constant "norm", lest it clash with the norm of a vector space
The file was modified src/HOL/Algebra/Generated_Groups.thy (diff)
The file was modified src/HOL/Algebra/Solvable_Groups.thy (diff)
Changeset 68575:d40d03487f64 by paulson _lp15@cam.ac.uk_:
more lemmas from Paulo
The file was modified src/HOL/Algebra/Multiplicative_Group.thy (diff)
Changeset 68574:0307cdca6462 by wenzelm:
merged
Changeset 68573:fb693268991a by wenzelm:
updated for release;
The file was modified Admin/Release/CHECKLIST (diff)
Changeset 68572:c8bf6077a87d by wenzelm:
Added tag Isabelle2018-RC1 for changeset cf01d04e94d7
The file was modified .hgtags (diff)
Changeset 68571:2a6e258bfd66 by paulson _lp15@cam.ac.uk_:
fixed (?) LaTeX presentation
The file was modified src/HOL/Algebra/Embedded_Algebras.thy (diff)
Changeset 68570:aa48b37092df by paulson:
merged
Changeset 68569:c64319959bab by paulson _lp15@cam.ac.uk_:
Lots of new algebra theories by Martin Baillon and Paulo Emílio de Vilhena
The file was addedsrc/HOL/Algebra/Algebra.thy
The file was addedsrc/HOL/Algebra/Chinese_Remainder.thy
The file was addedsrc/HOL/Algebra/Cycles.thy
The file was addedsrc/HOL/Algebra/Embedded_Algebras.thy
The file was addedsrc/HOL/Algebra/Generated_Fields.thy
The file was addedsrc/HOL/Algebra/Generated_Groups.thy
The file was addedsrc/HOL/Algebra/Generated_Rings.thy
The file was addedsrc/HOL/Algebra/Ideal_Product.thy
The file was addedsrc/HOL/Algebra/Solvable_Groups.thy
The file was addedsrc/HOL/Algebra/Subrings.thy
The file was addedsrc/HOL/Algebra/Sym_Groups.thy
The file was modified src/HOL/ROOT (diff)
Changeset 68568:cf01d04e94d7 by wenzelm:
more NEWS;
The file was modified NEWS (diff)
Changeset 68567:b408728a002a by wenzelm:
tuned;
The file was modified ANNOUNCE (diff)
Changeset 68566:38c8b44b40b9 by wenzelm:
more robust: avoid dire effect of ui.tweakoptions on hg.known_files;
The file was modified src/Pure/General/mercurial.scala (diff)
Changeset 68565:1b9462304e1d by blanchet:
update Sledgehammer docs w.r.t. Vampire
The file was modified src/Doc/Sledgehammer/document/root.tex (diff)
Changeset 68564:3ee6947bfb34 by blanchet:
added Vampire component
The file was modified Admin/components/components.sha1 (diff)
The file was modified Admin/components/main (diff)
Changeset 68563:05fb05f94686 by blanchet:
added option for noncommercial Vampire
The file was modified src/HOL/Tools/ATP/atp_systems.ML (diff)
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML (diff)
The file was modified src/HOL/Tools/etc/options (diff)