Skip to content
[Jenkins]Jenkins
log in
Aborted

Changes

Summary

  1. jenkins: pre/post-hook results
  2. Added missing Public_Announcement_Logic to ROOTS file
  3. More Support on Clean Syntax, Basic Lens Support, New Examples.
  4. finishing arg -> Arg and moving some material out of Stirling_Formula/Gamma_Asymptotics
  5. arg -> Arg: the last holdout
  6. merged
  7. arg -> Arg
  8. Add entry public announcement logic
  9. merged
  10. adapt to changes in HOL-Library.Cardinality
  11. Added Approximation_Algorithm for Center_Selection
  12. proved conditional completeness of compilation
  13. fixed typos
  14. more word cleanup
  15. more default simp rules
  16. some word streamlining
  17. made consistent again
  18. Fixed entry name for theories in sub-directory
Changeset 12499:869efd0ea35a by fabian huch _huch@in.tum.de_:
jenkins: pre/post-hook results
The file was modified admin/jenkins/ci_build_afp.scala (diff)
The file was modified admin/jenkins/ci_build_all.scala (diff)
The file was modified admin/jenkins/ci_build_mac.scala (diff)
The file was modified admin/jenkins/ci_build_slow.scala (diff)
The file was modified admin/jenkins/ci_build_testboard.scala (diff)
Changeset 12498:9c417896a51d by manuel eberl _eberlm@in.tum.de_:
Added missing Public_Announcement_Logic to ROOTS file
The file was modified thys/ROOTS (diff)
Changeset 12497:9070c70617f5 by Burkhart Wolff _wolff@lri.fr_:
More Support on Clean Syntax, Basic Lens Support, New Examples.
The file was addedthys/Clean/examples/IsPrime.thy
The file was addedthys/Clean/examples/LinearSearch.thy
The file was addedthys/Clean/examples/Quicksort.thy
The file was addedthys/Clean/src/Lens_Laws.thy
The file was addedthys/Clean/src/Optics.thy
The file was modified thys/Clean/ROOT (diff)
The file was modified thys/Clean/document/root.tex (diff)
The file was modified thys/Clean/examples/Quicksort_concept.thy (diff)
The file was modified thys/Clean/examples/SquareRoot_concept.thy (diff)
The file was modified thys/Clean/src/Clean.thy (diff)
The file was modified thys/Clean/src/Clean_Main.thy (diff)
The file was modified thys/Clean/src/Clean_Symbex.thy (diff)
The file was modified thys/Clean/src/Hoare_Clean.thy (diff)
The file was modified thys/Clean/src/Hoare_MonadSE.thy (diff)
The file was modified thys/Clean/src/MonadSE.thy (diff)
The file was modified thys/Clean/src/Symbex_MonadSE.thy (diff)
The file was modified thys/Clean/src/Test_Clean.thy (diff)
Changeset 12496:2ccc185fdaac by paulson _lp15@cam.ac.uk_:
finishing arg -> Arg and moving some material out of Stirling_Formula/Gamma_Asymptotics
The file was modified thys/Complex_Geometry/More_Complex.thy (diff)
The file was modified thys/Perron_Frobenius/Roots_Unity.thy (diff)
The file was modified thys/Stirling_Formula/Gamma_Asymptotics.thy (diff)
Changeset 12495:510c4df209cf by paulson _lp15@cam.ac.uk_:
arg -> Arg: the last holdout
The file was modified thys/Poincare_Disc/Poincare_Between.thy (diff)
The file was modified thys/Poincare_Disc/Poincare_Lines.thy (diff)
The file was modified thys/Poincare_Disc/Poincare_Lines_Axis_Intersections.thy (diff)
The file was modified thys/Poincare_Disc/Poincare_Tarski.thy (diff)
Changeset 12494:0a3968ac9ac6 by paulson:
merged
Changeset 12493:76eb5ab42012 by paulson _lp15@cam.ac.uk_:
arg -> Arg
The file was modified thys/Complex_Geometry/Angles.thy (diff)
The file was modified thys/Complex_Geometry/Circlines.thy (diff)
The file was modified thys/Complex_Geometry/Elementary_Complex_Geometry.thy (diff)
The file was modified thys/Complex_Geometry/Moebius.thy (diff)
The file was modified thys/Complex_Geometry/More_Complex.thy (diff)
The file was modified thys/Complex_Geometry/Oriented_Circlines.thy (diff)
The file was modified thys/Complex_Geometry/Unit_Circle_Preserving_Moebius.thy (diff)
The file was modified thys/Complex_Geometry/Unitary11_Matrices.thy (diff)
The file was modified thys/Lambda_Free_KBOs/Lambda_Free_TKBO_Coefs.thy (diff)
The file was modified thys/Lambda_Free_RPOs/Lambda_Free_Util.thy (diff)
The file was modified thys/Perron_Frobenius/Perron_Frobenius_Irreducible.thy (diff)
The file was modified thys/Perron_Frobenius/Roots_Unity.thy (diff)
The file was modified thys/Poincare_Disc/Poincare_Between.thy (diff)
The file was modified thys/Poincare_Disc/Poincare_Tarski.thy (diff)
The file was modified thys/Stirling_Formula/Gamma_Asymptotics.thy (diff)
Changeset 12492:3e122937ba1a by asta halkjær from _andro.from@gmail.com_:
Add entry public announcement logic
The file was addedthys/Public_Announcement_Logic/PAL.thy
The file was addedthys/Public_Announcement_Logic/ROOT
The file was addedthys/Public_Announcement_Logic/document/root.bib
The file was addedthys/Public_Announcement_Logic/document/root.tex
The file was modified metadata/metadata (diff)
Changeset 12491:718cb448a456 by andreas lochbihler _mail@andreas-lochbihler.de_:
merged
Changeset 12490:20bc49db635f by andreas lochbihler _mail@andreas-lochbihler.de_:
adapt to changes in HOL-Library.Cardinality
The file was modified thys/Affine_Arithmetic/Executable_Euclidean_Space.thy (diff)
The file was modified thys/Containers/Containers_Userguide.thy (diff)
The file was modified thys/Containers/ITP-2013/Benchmark_Set_Default.thy (diff)
The file was modified thys/Containers/ITP-2013/Benchmark_Set_LC.thy (diff)
The file was modified thys/Containers/Set_Impl.thy (diff)
The file was modified thys/Extended_Finite_State_Machine_Inference/code-targets/Code_Target_Set.thy (diff)
The file was modified thys/Gauss_Jordan/Code_Set.thy (diff)
The file was modified thys/JinjaThreads/Execute/Code_Generation.thy (diff)
The file was modified thys/JinjaThreads/Execute/Java2Jinja.thy (diff)
The file was modified thys/MFODL_Monitor_Optimized/Monitor_Impl.thy (diff)
The file was modified thys/Physical_Quantities/Enum_extra.thy (diff)
Changeset 12489:c4a38a2daedf by nipkow:
Added Approximation_Algorithm for Center_Selection
The file was addedthys/Approximation_Algorithms/Center_Selection.thy
The file was modified metadata/metadata (diff)
The file was modified thys/Approximation_Algorithms/ROOT (diff)
The file was modified thys/Approximation_Algorithms/document/root.tex (diff)
The file was modified web/entries/Aggregation_Algebras.html (diff)
The file was modified web/entries/Approximation_Algorithms.html (diff)
The file was modified web/entries/Epistemic_Logic.html (diff)
The file was modified web/entries/Interpreter_Optimizations.html (diff)
The file was modified web/entries/Relational_Disjoint_Set_Forests.html (diff)
The file was modified web/entries/Stone_Relation_Algebras.html (diff)
The file was modified web/index.html (diff)
The file was modified web/statistics.html (diff)
Changeset 12486:5695f90acdbf by desharna:
proved conditional completeness of compilation
The file was addedthys/Interpreter_Optimizations/Inca_Verification.thy
The file was modified metadata/metadata (diff)
The file was modified thys/Interpreter_Optimizations/Global.thy (diff)
The file was modified thys/Interpreter_Optimizations/Inca.thy (diff)
The file was modified thys/Interpreter_Optimizations/Inca_to_Ubx_compiler.thy (diff)
The file was modified thys/Interpreter_Optimizations/List_util.thy (diff)
The file was modified thys/Interpreter_Optimizations/Map_Extra.thy (diff)
The file was modified thys/Interpreter_Optimizations/Op_example.thy (diff)
The file was modified thys/Interpreter_Optimizations/Std.thy (diff)
The file was modified thys/Interpreter_Optimizations/Std_to_Inca_compiler.thy (diff)
The file was modified thys/Interpreter_Optimizations/Ubx.thy (diff)
Changeset 12485:e8af416c2e70 by nipkow:
fixed typos
The file was modified thys/Amortized_Complexity/Amortized_Framework0.thy (diff)
Changeset 12484:1a99ac2d4342 by haftmann:
more word cleanup
The file was modified thys/Native_Word/Code_Symbolic_Bits_Int.thy (diff)
The file was modified thys/Native_Word/More_Bits_Int.thy (diff)
The file was modified thys/Word_Lib/Bits_Int.thy (diff)
The file was modified thys/Word_Lib/Generic_set_bit.thy (diff)
The file was modified thys/Word_Lib/More_Arithmetic.thy (diff)
The file was modified thys/Word_Lib/Most_significant_bit.thy (diff)
The file was modified thys/Word_Lib/Norm_Words.thy (diff)
The file was modified thys/Word_Lib/Signed_Division_Word.thy (diff)
The file was modified thys/Word_Lib/Word_Lemmas.thy (diff)
Changeset 12483:f1195cc96e85 by haftmann:
more default simp rules
The file was modified thys/AVL-Trees/AVL.thy (diff)
The file was modified thys/Akra_Bazzi/Akra_Bazzi_Asymptotics.thy (diff)
The file was modified thys/BTree/BTree_ImpSet.thy (diff)
The file was modified thys/BenOr_Kozen_Reif/BKR_Proofs.thy (diff)
The file was modified thys/Berlekamp_Zassenhaus/Mahler_Measure.thy (diff)
The file was modified thys/Bertrands_Postulate/Bertrand.thy (diff)
The file was modified thys/Chandy_Lamport/Co_Snapshot.thy (diff)
The file was modified thys/Closest_Pair_Points/Common.thy (diff)
The file was modified thys/Coinductive/Coinductive_Nat.thy (diff)
The file was modified thys/Dirichlet_Series/Dirichlet_Series_Analysis.thy (diff)
The file was modified thys/Ergodic_Theory/Kingman.thy (diff)
The file was modified thys/Extended_Finite_State_Machines/GExp.thy (diff)
The file was modified thys/Gromov_Hyperbolicity/Gromov_Hyperbolicity.thy (diff)
The file was modified thys/Group-Ring-Module/Algebra5.thy (diff)
The file was modified thys/Group-Ring-Module/Algebra6.thy (diff)
The file was modified thys/HereditarilyFinite/HF.thy (diff)
The file was modified thys/IP_Addresses/IPv6.thy (diff)
The file was modified thys/Inductive_Inference/Universal.thy (diff)
The file was modified thys/JinjaThreads/MM/SC_Completion.thy (diff)
The file was modified thys/List-Infinite/ListInf/List2.thy (diff)
The file was modified thys/List_Update/Move_to_Front.thy (diff)
The file was modified thys/Locally-Nameless-Sigma/preliminary/ListPre.thy (diff)
The file was modified thys/Lp/Lp.thy (diff)
The file was modified thys/Noninterference_CSP/ClassicalNoninterference.thy (diff)
The file was modified thys/Ordinal_Partitions/Erdos_Milner.thy (diff)
The file was modified thys/Prime_Distribution_Elementary/More_Dirichlet_Misc.thy (diff)
The file was modified thys/Prime_Number_Theorem/Mertens_Theorems.thy (diff)
The file was modified thys/Probabilistic_Noninterference/Language_Semantics.thy (diff)
The file was modified thys/RSAPSS/Word.thy (diff)
The file was modified thys/Recursion-Theory-I/PRecFinSet.thy (diff)
The file was modified thys/Simple_Firewall/Primitives/Iface.thy (diff)
The file was modified thys/Taylor_Models/Polynomial_Expression_Additional.thy (diff)
The file was modified thys/Timed_Automata/Approx_Beta.thy (diff)
The file was modified thys/Timed_Automata/Paths_Cycles.thy (diff)
The file was modified thys/Universal_Turing_Machine/Recursive.thy (diff)
The file was modified thys/Word_Lib/More_Arithmetic.thy (diff)
The file was modified thys/Zeta_Function/Zeta_Library.thy (diff)
The file was modified thys/pGCL/Tutorial/Primitives.thy (diff)
Changeset 12482:9e42e0c5f9f9 by haftmann:
some word streamlining
The file was modified thys/Word_Lib/Bits_Int.thy (diff)
Changeset 12481:55af834ad1b8 by haftmann:
made consistent again
The file was modified thys/Group-Ring-Module/Algebra5.thy (diff)
Changeset 12480:291a8d8961b4 by fabian huch _huch@in.tum.de_:
Fixed entry name for theories in sub-directory
The file was modified admin/jenkins/ci_build_all.scala (diff)
The file was modified admin/jenkins/ci_build_testboard.scala (diff)