Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. merged
  2. Makefile is no longer needed ("isabelle afp_build HLDE" generates binary "generated/hlde" as specified in Solve_Code.thy by Florian Haftmann
  3. tuned proofs
  4. updated op's
  5. adapted to reverted <= syntax
  6. merged
  7. updated op syntax
  8. dropped more lemmas that are now already part of Main
  9. merged
  10. reuse lemmas that are now in Main
  11. merged
  12. updated to backed out infixes in Set & Ordereings
Changeset 8719:6cd86a964944 by Christian Sternagel:
merged
Changeset 8718:90fe663df88e by Christian Sternagel:
Makefile is no longer needed (&quot;isabelle afp_build HLDE&quot; generates binary &quot;generated/hlde&quot; as specified in Solve_Code.thy by Florian Haftmann
The file was removedthys/Diophantine_Eqns_Lin_Hom/Makefile
Changeset 8717:aac9903ef36c by Christian Sternagel:
tuned proofs
The file was modified thys/Diophantine_Eqns_Lin_Hom/List_Vector.thy (diff)
Changeset 8716:545001eddbc5 by nipkow:
updated op&#039;s
The file was modified thys/Stochastic_Matrices/Stochastic_Matrix.thy (diff)
The file was modified thys/Stochastic_Matrices/Stochastic_Vector_PMF.thy (diff)
Changeset 8715:7b80d0c6e88e by nipkow:
adapted to reverted &lt;= syntax
The file was modified thys/KAT_and_DRA/SingleSorted/DRA_Models.thy (diff)
Changeset 8714:fec73e58a948 by nipkow:
merged
Changeset 8713:43a44bb8db11 by nipkow:
updated op syntax
The file was modified thys/Taylor_Models/Polynomial_Expression_Additional.thy (diff)
The file was modified thys/Taylor_Models/Taylor_Models.thy (diff)
The file was modified thys/Taylor_Models/Taylor_Models_Misc.thy (diff)
Changeset 8712:b9d00590c21f by Christian Sternagel:
dropped more lemmas that are now already part of Main
The file was modified thys/Diophantine_Eqns_Lin_Hom/List_Vector.thy (diff)
Changeset 8711:a2248939ff2c by Christian Sternagel:
merged
Changeset 8710:86c1f53a9f02 by Christian Sternagel:
reuse lemmas that are now in Main
The file was modified thys/Diophantine_Eqns_Lin_Hom/Algorithm.thy (diff)
The file was modified thys/Diophantine_Eqns_Lin_Hom/List_Vector.thy (diff)
The file was modified thys/Diophantine_Eqns_Lin_Hom/Simple_Algorithm.thy (diff)
Changeset 8709:64ca544f28b2 by nipkow:
merged
Changeset 8708:c0329b30ef3f by nipkow:
updated to backed out infixes in Set &amp; Ordereings
The file was modified thys/HOLCF-Prelude/Data_List.thy (diff)
The file was modified thys/Lp/Functional_Spaces.thy (diff)
The file was modified thys/Nested_Multisets_Ordinals/Signed_Multiset.thy (diff)