Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

Summary

  1. merged
  2. clarified signature;
  3. confluent preprocessing for floats in presence of target language numerals
  4. subclass relation
Changeset 73548:c54a9395ad96 by wenzelm:
merged
Changeset 73547:a7aabdf889b7 by wenzelm:
clarified signature;
The file was modified src/HOL/SPARK/Tools/spark_vcs.ML
The file was modified src/Pure/General/http.scala
The file was modified src/Pure/System/isabelle_system.ML
The file was modified src/Pure/System/isabelle_system.scala
Changeset 73546:7cb3fefef79e by haftmann:
confluent preprocessing for floats in presence of target language numerals
The file was addedsrc/HOL/Library/Code_Target_Numeral_Float.thy
The file was modified src/HOL/Decision_Procs/Approximation.thy
The file was modified src/HOL/ROOT
Changeset 73545:fc72e5ebf9de by haftmann:
subclass relation
The file was modified src/HOL/Rings.thy

Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

Summary

  1. clarified message, following Isabelle/a7aabdf889b7;
  2. confluent preprocessing for floats in presence of target language numerals
  3. subclass relation
Changeset 11719:107ecc8216a8 by wenzelm:
clarified message, following Isabelle/a7aabdf889b7;
The file was modified thys/Network_Security_Policy_Verification/TopoS_generateCode.thy
Changeset 11718:c351b9b63b58 by haftmann:
confluent preprocessing for floats in presence of target language numerals
Changeset 11717:b3ff22dfc82d by haftmann:
subclass relation
The file was modified thys/Ergodic_Theory/SG_Library_Complement.thy
The file was modified thys/LLL_Basis_Reduction/Missing_Lemmas.thy