Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. merged
  2. adapted to renamed suffix
  3. isabelle update_cartouches -c -t;
  4. updated 'define';
  5. exploit validity of factorization oracle
  6. wrapper of rational polynomial factorization oracle ensures square-free factors and validity
  7. square-free is now defined for 'a :: idom poly (instead of 'a :: field poly)
  8. listprod_dvd
Changeset 6681:7283d8fa2b9c by nipkow:
merged
Changeset 6680:d50c3f832fe0 by nipkow:
adapted to renamed suffix
The file was modified thys/ConcurrentGC/Tactics.thy (diff)
The file was modified thys/Formal_SSA/Construct_SSA_notriv.thy (diff)
The file was modified thys/Formal_SSA/FormalSSA_Misc.thy (diff)
The file was modified thys/Formal_SSA/Graph_path.thy (diff)
The file was modified thys/Formal_SSA/Minimality.thy (diff)
The file was modified thys/Formal_SSA/SSA_CFG.thy (diff)
The file was modified thys/Formal_SSA/SSA_Semantics.thy (diff)
The file was modified thys/JinjaThreads/Compiler/TypeComp.thy (diff)
The file was modified thys/Well_Quasi_Orders/Higman_OI.thy (diff)
Changeset 6679:bf5464a82ecc by wenzelm:
isabelle update_cartouches -c -t;
The file was modified thys/Simpl/AlternativeSmallStep.thy (diff)
The file was modified thys/Simpl/DPC0Expressions.thy (diff)
The file was modified thys/Simpl/DPC0Library.thy (diff)
The file was modified thys/Simpl/HeapList.thy (diff)
The file was modified thys/Simpl/Hoare.thy (diff)
The file was modified thys/Simpl/HoarePartial.thy (diff)
The file was modified thys/Simpl/HoarePartialDef.thy (diff)
The file was modified thys/Simpl/HoarePartialProps.thy (diff)
The file was modified thys/Simpl/HoareTotal.thy (diff)
The file was modified thys/Simpl/HoareTotalDef.thy (diff)
The file was modified thys/Simpl/HoareTotalProps.thy (diff)
The file was modified thys/Simpl/Language.thy (diff)
The file was modified thys/Simpl/Semantic.thy (diff)
The file was modified thys/Simpl/Simpl_Heap.thy (diff)
The file was modified thys/Simpl/SmallStep.thy (diff)
The file was modified thys/Simpl/StateSpace.thy (diff)
The file was modified thys/Simpl/Termination.thy (diff)
The file was modified thys/Simpl/UserGuide.thy (diff)
The file was modified thys/Simpl/Vcg.thy (diff)
The file was modified thys/Simpl/XVcg.thy (diff)
The file was modified thys/Simpl/ex/Closure.thy (diff)
The file was modified thys/Simpl/ex/Compose.thy (diff)
The file was modified thys/Simpl/ex/VcgEx.thy (diff)
The file was modified thys/Simpl/ex/VcgExSP.thy (diff)
The file was modified thys/Simpl/ex/VcgExTotal.thy (diff)
Changeset 6678:585368e5f105 by wenzelm:
updated 'define';
The file was modified thys/Simpl/AlternativeSmallStep.thy (diff)
The file was modified thys/Simpl/HoareTotalProps.thy (diff)
The file was modified thys/Simpl/SmallStep.thy (diff)
The file was modified thys/Simpl/ex/VcgEx.thy (diff)
The file was modified thys/Simpl/ex/VcgExSP.thy (diff)
Changeset 6677:9fc086c454ff by rene thiemann _rene.thiemann@uibk.ac.at_:
exploit validity of factorization oracle
The file was modified thys/Polynomial_Factorization/Rational_Factorization.thy (diff)
Changeset 6676:a11ccf8491b7 by rene thiemann _rene.thiemann@uibk.ac.at_:
wrapper of rational polynomial factorization oracle ensures square-free factors and validity
The file was modified thys/Polynomial_Factorization/Factorization_Oracle.thy (diff)
Changeset 6675:731c4ae04e24 by rene thiemann _rene.thiemann@uibk.ac.at_:
square-free is now defined for 'a :: idom poly (instead of 'a :: field poly)
The file was modified thys/Polynomial_Factorization/Square_Free_Factorization.thy (diff)
Changeset 6674:5b1216cfd4b4 by rene thiemann _rene.thiemann@uibk.ac.at_:
listprod_dvd
The file was modified thys/Polynomial_Interpolation/Missing_Unsorted.thy (diff)