Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. Fixed for renamed theorems, etc.
  2. rename and simplify
  3. repair the optimization on chars when generating a deep-certificate
  4. merge from afp-2016
  5. point to bitbucket instead of SF
  6. merge from afp-2016
  7. new submission system
  8. new submission system
  9. merged
  10. missing AFP
  11. PropResPI webpage
  12. new entry PropResPI
  13. new article Timed-Automata
  14. tuned
  15. new entry Cartan_FP
  16. New entry LTL
  17. update links to older (2015) releases
  18. added missing List_Update entry page
  19. import List_Update from afp-devel
  20. record 2015 releases, bump Isabelle version to 2016
  21. website to release mode (afp-2016)
  22. unified CHAR with CHR syntax
  23. adapted to recent Multiset change
Changeset 6462:08ba67fd78a0 by paulson _lp15@cam.ac.uk_:
Fixed for renamed theorems, etc.
The file was modified thys/Cartan_FP/Cartan.thy (diff)
Changeset 6461:0a24209202cc by frédéric tuong _frederic.tuong@{u-psud,irt-systemx,lri}.fr_:
rename and simplify
The file was modified thys/Isabelle_Meta_Model/Init.thy (diff)
The file was modified thys/Isabelle_Meta_Model/toy_example/embedding/core/Core_init.thy (diff)
The file was modified thys/Isabelle_Meta_Model/toy_example/embedding/core/Floor1_access.thy (diff)
The file was modified thys/Isabelle_Meta_Model/toy_example/embedding/core/Floor1_examp.thy (diff)
The file was modified thys/Isabelle_Meta_Model/toy_example/embedding/core/Floor2_examp.thy (diff)
The file was modified thys/Isabelle_Meta_Model/toy_example/embedding/meta_toy/Parser_META.thy (diff)
Changeset 6460:25f867a6067c by frédéric tuong _frederic.tuong@{u-psud,irt-systemx,lri}.fr_:
repair the optimization on chars when generating a deep-certificate
The file was modified thys/Isabelle_Meta_Model/Init.thy (diff)
The file was modified thys/Isabelle_Meta_Model/toy_example/embedding/meta_toy/Parser_META.thy (diff)
Changeset 6459:ada7aa0acf0b by kleing:
merge from afp-2016
Changeset 6458:d09c62ecc43a by gerwin.klein@nicta.com.au:
point to bitbucket instead of SF
The file was modified admin/mkstatus.py (diff)
Changeset 6457:e0185aebe4ed by kleing:
merge from afp-2016
Changeset 6456:6982c5d2c8f8 by nipkow:
new submission system
The file was modified thys/Example-Submission/Submission.thy (diff)
Changeset 6455:6d8c69f873a9 by nipkow:
new submission system
The file was modified web/submitting.shtml (diff)
Changeset 6454:191c4bea4c4f by nipkow:
merged
Changeset 6453:439258c4ce94 by nipkow:
missing AFP
The file was modified thys/Timed_Automata/ROOT (diff)
Changeset 6452:58b0e0c803ab by paulson _lp15@cam.ac.uk_:
PropResPI webpage
The file was addedweb/entries/PropResPI.shtml
The file was modified metadata/metadata (diff)
The file was modified web/index.shtml (diff)
The file was modified web/topics.shtml (diff)
Changeset 6451:696e8616a9e6 by paulson _lp15@cam.ac.uk_:
new entry PropResPI
The file was addedthys/PropResPI/Prime_Implicates.thy
The file was addedthys/PropResPI/Propositional_Resolution.thy
The file was addedthys/PropResPI/ROOT
The file was addedthys/PropResPI/config
The file was addedthys/PropResPI/document/root.tex
The file was modified thys/ROOTS (diff)
Changeset 6450:a4327c8e61df by nipkow:
new article Timed-Automata
The file was addedthys/Timed_Automata/Approx_Beta.thy
The file was addedthys/Timed_Automata/Closure.thy
The file was addedthys/Timed_Automata/DBM.thy
The file was addedthys/Timed_Automata/DBM_Basics.thy
The file was addedthys/Timed_Automata/DBM_Normalization.thy
The file was addedthys/Timed_Automata/DBM_Operations.thy
The file was addedthys/Timed_Automata/DBM_Zone_Semantics.thy
The file was addedthys/Timed_Automata/Floyd_Warshall.thy
The file was addedthys/Timed_Automata/Misc.thy
The file was addedthys/Timed_Automata/Normalized_Zone_Semantics.thy
The file was addedthys/Timed_Automata/Paths_Cycles.thy
The file was addedthys/Timed_Automata/ROOT
The file was addedthys/Timed_Automata/Regions.thy
The file was addedthys/Timed_Automata/Regions_Beta.thy
The file was addedthys/Timed_Automata/Timed_Automata.thy
The file was addedthys/Timed_Automata/config
The file was addedthys/Timed_Automata/document/root.bib
The file was addedthys/Timed_Automata/document/root.tex
The file was addedweb/entries/Timed_Automata.shtml
The file was modified metadata/metadata (diff)
The file was modified thys/ROOTS (diff)
The file was modified web/index.shtml (diff)
The file was modified web/topics.shtml (diff)
Changeset 6449:f370d197e854 by nipkow:
tuned
The file was modified metadata/metadata (diff)
The file was modified web/entries/Cartan_FP.shtml (diff)
Changeset 6448:b72bc01eed3f by nipkow:
new entry Cartan_FP
The file was addedthys/Cartan_FP/Cartan.thy
The file was addedthys/Cartan_FP/ROOT
The file was addedthys/Cartan_FP/document/root.bib
The file was addedthys/Cartan_FP/document/root.tex
The file was addedweb/entries/Cartan_FP.shtml
The file was modified metadata/metadata (diff)
The file was modified thys/ROOTS (diff)
The file was modified web/index.shtml (diff)
The file was modified web/topics.shtml (diff)
Changeset 6447:38de4f7e4d60 by nipkow:
New entry LTL
The file was addedthys/LTL/LTL.thy
The file was addedthys/LTL/LTL_Rewrite.thy
The file was addedthys/LTL/ROOT
The file was addedthys/LTL/config
The file was addedthys/LTL/document/root.bib
The file was addedthys/LTL/document/root.tex
The file was addedthys/LTL/example/LTL_Example.thy
The file was addedthys/LTL/example/build_poly.sh
The file was addedthys/LTL/example/rewrite_example.sml
The file was addedthys/LTL/example/rewrite_example_cli.sml
The file was addedthys/LTL/example/rewrite_example_poly.sml
The file was addedthys/LTL/parser/compiler.sml
The file was addedthys/LTL/parser/datatypes.sml
The file was addedthys/LTL/parser/glue.sml
The file was addedthys/LTL/parser/ltl.lex
The file was addedthys/LTL/parser/ltl.lex.sml
The file was addedthys/LTL/parser/ltl.yacc
The file was addedthys/LTL/parser/ltl.yacc.sig
The file was addedthys/LTL/parser/ltl.yacc.sml
The file was addedweb/entries/LTL.shtml
The file was modified metadata/metadata (diff)
The file was modified thys/ROOTS (diff)
The file was modified web/index.shtml (diff)
The file was modified web/topics.shtml (diff)
Changeset 6446:2d574f8c1263 by gerwin.klein@nicta.com.au:
update links to older (2015) releases
The file was modified metadata/release-dates (diff)
The file was modified metadata/releases (diff)
The file was modified web/entries/AODV.shtml (diff)
The file was modified web/entries/AVL-Trees.shtml (diff)
The file was modified web/entries/AWN.shtml (diff)
The file was modified web/entries/Abortable_Linearizable_Modules.shtml (diff)
The file was modified web/entries/Abstract-Hoare-Logics.shtml (diff)
The file was modified web/entries/Abstract-Rewriting.shtml (diff)
The file was modified web/entries/Abstract_Completeness.shtml (diff)
The file was modified web/entries/Affine_Arithmetic.shtml (diff)
The file was modified web/entries/Akra_Bazzi.shtml (diff)
The file was modified web/entries/Algebraic_Numbers.shtml (diff)
The file was modified web/entries/Amortized_Complexity.shtml (diff)
The file was modified web/entries/Applicative_Lifting.shtml (diff)
The file was modified web/entries/ArrowImpossibilityGS.shtml (diff)
The file was modified web/entries/AutoFocus-Stream.shtml (diff)
The file was modified web/entries/Automatic_Refinement.shtml (diff)
The file was modified web/entries/BDD.shtml (diff)
The file was modified web/entries/BinarySearchTree.shtml (diff)
The file was modified web/entries/Binomial-Heaps.shtml (diff)
The file was modified web/entries/Binomial-Queues.shtml (diff)
The file was modified web/entries/Bondy.shtml (diff)
The file was modified web/entries/Boolean_Expression_Checkers.shtml (diff)
The file was modified web/entries/Bounded_Deducibility_Security.shtml (diff)
The file was modified web/entries/BytecodeLogicJmlTypes.shtml (diff)
The file was modified web/entries/CAVA_Automata.shtml (diff)
The file was modified web/entries/CAVA_LTL_Modelchecker.shtml (diff)
The file was modified web/entries/CCS.shtml (diff)
The file was modified web/entries/CISC-Kernel.shtml (diff)
The file was modified web/entries/Call_Arity.shtml (diff)
The file was modified web/entries/Card_Number_Partitions.shtml (diff)
The file was modified web/entries/Card_Partitions.shtml (diff)
The file was modified web/entries/Case_Labeling.shtml (diff)
The file was modified web/entries/Category.shtml (diff)
The file was modified web/entries/Category2.shtml (diff)
The file was modified web/entries/Cauchy.shtml (diff)
The file was modified web/entries/Cayley_Hamilton.shtml (diff)
The file was modified web/entries/Certification_Monads.shtml (diff)
The file was modified web/entries/Circus.shtml (diff)
The file was modified web/entries/ClockSynchInst.shtml (diff)
The file was modified web/entries/CofGroups.shtml (diff)
The file was modified web/entries/Coinductive.shtml (diff)
The file was modified web/entries/Coinductive_Languages.shtml (diff)
The file was modified web/entries/Collections.shtml (diff)
The file was modified web/entries/Compiling-Exceptions-Correctly.shtml (diff)
The file was modified web/entries/Completeness.shtml (diff)
The file was modified web/entries/ComponentDependencies.shtml (diff)
The file was modified web/entries/ConcurrentGC.shtml (diff)
The file was modified web/entries/ConcurrentIMP.shtml (diff)
The file was modified web/entries/Consensus_Refined.shtml (diff)
The file was modified web/entries/Containers.shtml (diff)
The file was modified web/entries/CoreC++.shtml (diff)
The file was modified web/entries/CryptoBasedCompositionalProperties.shtml (diff)
The file was modified web/entries/DPT-SAT-Solver.shtml (diff)
The file was modified web/entries/DataRefinementIBP.shtml (diff)
The file was modified web/entries/Datatype_Order_Generator.shtml (diff)
The file was modified web/entries/Decreasing-Diagrams-II.shtml (diff)
The file was modified web/entries/Decreasing-Diagrams.shtml (diff)
The file was modified web/entries/Density_Compiler.shtml (diff)
The file was modified web/entries/Depth-First-Search.shtml (diff)
The file was modified web/entries/Derangements.shtml (diff)
The file was modified web/entries/Deriving.shtml (diff)
The file was modified web/entries/Descartes_Sign_Rule.shtml (diff)
The file was modified web/entries/Dijkstra_Shortest_Path.shtml (diff)
The file was modified web/entries/Discrete_Summation.shtml (diff)
The file was modified web/entries/DiskPaxos.shtml (diff)
The file was modified web/entries/Dynamic_Tables.shtml (diff)
The file was modified web/entries/Echelon_Form.shtml (diff)
The file was modified web/entries/Efficient-Mergesort.shtml (diff)
The file was modified web/entries/Encodability_Process_Calculi.shtml (diff)
The file was modified web/entries/Euler_Partition.shtml (diff)
The file was modified web/entries/FFT.shtml (diff)
The file was modified web/entries/FOL-Fitting.shtml (diff)
The file was modified web/entries/FeatherweightJava.shtml (diff)
The file was modified web/entries/Featherweight_OCL.shtml (diff)
The file was modified web/entries/Fermat3_4.shtml (diff)
The file was modified web/entries/FileRefinement.shtml (diff)
The file was modified web/entries/FinFun.shtml (diff)
The file was modified web/entries/Finger-Trees.shtml (diff)
The file was modified web/entries/Finite_Automata_HF.shtml (diff)
The file was modified web/entries/Flyspeck-Tame.shtml (diff)
The file was modified web/entries/FocusStreamsCaseStudies.shtml (diff)
The file was modified web/entries/Formal_SSA.shtml (diff)
The file was modified web/entries/Formula_Derivatives.shtml (diff)
The file was modified web/entries/Free-Boolean-Algebra.shtml (diff)
The file was modified web/entries/Free-Groups.shtml (diff)
The file was modified web/entries/FunWithFunctions.shtml (diff)
The file was modified web/entries/FunWithTilings.shtml (diff)
The file was modified web/entries/Functional-Automata.shtml (diff)
The file was modified web/entries/GPU_Kernel_PL.shtml (diff)
The file was modified web/entries/Gabow_SCC.shtml (diff)
The file was modified web/entries/Gauss-Jordan-Elim-Fun.shtml (diff)
The file was modified web/entries/Gauss_Jordan.shtml (diff)
The file was modified web/entries/GenClock.shtml (diff)
The file was modified web/entries/General-Triangle.shtml (diff)
The file was modified web/entries/Girth_Chromatic.shtml (diff)
The file was modified web/entries/GoedelGod.shtml (diff)
The file was modified web/entries/GraphMarkingIBP.shtml (diff)
The file was modified web/entries/Graph_Theory.shtml (diff)
The file was modified web/entries/Group-Ring-Module.shtml (diff)
The file was modified web/entries/HRB-Slicing.shtml (diff)
The file was modified web/entries/Heard_Of.shtml (diff)
The file was modified web/entries/HereditarilyFinite.shtml (diff)
The file was modified web/entries/Hermite.shtml (diff)
The file was modified web/entries/HotelKeyCards.shtml (diff)
The file was modified web/entries/Huffman.shtml (diff)
The file was modified web/entries/HyperCTL.shtml (diff)
The file was modified web/entries/IEEE_Floating_Point.shtml (diff)
The file was modified web/entries/Imperative_Insertion_Sort.shtml (diff)
The file was modified web/entries/Impossible_Geometry.shtml (diff)
The file was modified web/entries/Incompleteness.shtml (diff)
The file was modified web/entries/Inductive_Confidentiality.shtml (diff)
The file was modified web/entries/InformationFlowSlicing.shtml (diff)
The file was modified web/entries/Integration.shtml (diff)
The file was modified web/entries/Isabelle_Meta_Model.shtml (diff)
The file was modified web/entries/Jinja.shtml (diff)
The file was modified web/entries/JinjaThreads.shtml (diff)
The file was modified web/entries/JiveDataStoreModel.shtml (diff)
The file was modified web/entries/Jordan_Hoelder.shtml (diff)
The file was modified web/entries/Jordan_Normal_Form.shtml (diff)
The file was modified web/entries/KAT_and_DRA.shtml (diff)
The file was modified web/entries/KBPs.shtml (diff)
The file was modified web/entries/Kleene_Algebra.shtml (diff)
The file was modified web/entries/Knot_Theory.shtml (diff)
The file was modified web/entries/Koenigsberg_Friendship.shtml (diff)
The file was modified web/entries/LTL_to_DRA.shtml (diff)
The file was modified web/entries/LTL_to_GBA.shtml (diff)
The file was modified web/entries/Lam-ml-Normalization.shtml (diff)
The file was modified web/entries/Landau_Symbols.shtml (diff)
The file was modified web/entries/Latin_Square.shtml (diff)
The file was modified web/entries/LatticeProperties.shtml (diff)
The file was modified web/entries/Launchbury.shtml (diff)
The file was modified web/entries/Lazy-Lists-II.shtml (diff)
The file was modified web/entries/Lehmer.shtml (diff)
The file was modified web/entries/Lifting_Definition_Option.shtml (diff)
The file was modified web/entries/LightweightJava.shtml (diff)
The file was modified web/entries/LinearQuantifierElim.shtml (diff)
The file was modified web/entries/Liouville_Numbers.shtml (diff)
The file was modified web/entries/List-Index.shtml (diff)
The file was modified web/entries/List-Infinite.shtml (diff)
The file was modified web/entries/List_Interleaving.shtml (diff)
The file was modified web/entries/Locally-Nameless-Sigma.shtml (diff)
The file was modified web/entries/Lower_Semicontinuous.shtml (diff)
The file was modified web/entries/MSO_Regex_Equivalence.shtml (diff)
The file was modified web/entries/Markov_Models.shtml (diff)
The file was modified web/entries/Marriage.shtml (diff)
The file was modified web/entries/Matrix.shtml (diff)
The file was modified web/entries/Matrix_Tensor.shtml (diff)
The file was modified web/entries/Max-Card-Matching.shtml (diff)
The file was modified web/entries/MiniML.shtml (diff)
The file was modified web/entries/MonoBoolTranAlgebra.shtml (diff)
The file was modified web/entries/MuchAdoAboutTwo.shtml (diff)
The file was modified web/entries/Multirelations.shtml (diff)
The file was modified web/entries/Myhill-Nerode.shtml (diff)
The file was modified web/entries/Nat-Interval-Logic.shtml (diff)
The file was modified web/entries/Native_Word.shtml (diff)
The file was modified web/entries/Network_Security_Policy_Verification.shtml (diff)
The file was modified web/entries/Noninterference_CSP.shtml (diff)
The file was modified web/entries/Noninterference_Generic_Unwinding.shtml (diff)
The file was modified web/entries/Noninterference_Inductive_Unwinding.shtml (diff)
The file was modified web/entries/Noninterference_Ipurge_Unwinding.shtml (diff)
The file was modified web/entries/NormByEval.shtml (diff)
The file was modified web/entries/Open_Induction.shtml (diff)
The file was modified web/entries/Ordinal.shtml (diff)
The file was modified web/entries/Ordinals_and_Cardinals.shtml (diff)
The file was modified web/entries/Ordinary_Differential_Equations.shtml (diff)
The file was modified web/entries/PCF.shtml (diff)
The file was modified web/entries/POPLmark-deBruijn.shtml (diff)
The file was modified web/entries/Parity_Game.shtml (diff)
The file was modified web/entries/Partial_Function_MR.shtml (diff)
The file was modified web/entries/Perfect-Number-Thm.shtml (diff)
The file was modified web/entries/Pi_Calculus.shtml (diff)
The file was modified web/entries/Polynomials.shtml (diff)
The file was modified web/entries/Pop_Refinement.shtml (diff)
The file was modified web/entries/Possibilistic_Noninterference.shtml (diff)
The file was modified web/entries/Pratt_Certificate.shtml (diff)
The file was modified web/entries/Presburger-Automata.shtml (diff)
The file was modified web/entries/Prime_Harmonic_Series.shtml (diff)
The file was modified web/entries/Priority_Queue_Braun.shtml (diff)
The file was modified web/entries/Probabilistic_Noninterference.shtml (diff)
The file was modified web/entries/Probabilistic_System_Zoo.shtml (diff)
The file was modified web/entries/Program-Conflict-Analysis.shtml (diff)
The file was modified web/entries/Promela.shtml (diff)
The file was modified web/entries/PseudoHoops.shtml (diff)
The file was modified web/entries/Psi_Calculi.shtml (diff)
The file was modified web/entries/QR_Decomposition.shtml (diff)
The file was modified web/entries/RIPEMD-160-SPARK.shtml (diff)
The file was modified web/entries/RSAPSS.shtml (diff)
The file was modified web/entries/Ramsey-Infinite.shtml (diff)
The file was modified web/entries/Random_Graph_Subgraph_Threshold.shtml (diff)
The file was modified web/entries/Rank_Nullity_Theorem.shtml (diff)
The file was modified web/entries/Real_Impl.shtml (diff)
The file was modified web/entries/Recursion-Theory-I.shtml (diff)
The file was modified web/entries/Refine_Monadic.shtml (diff)
The file was modified web/entries/RefinementReactive.shtml (diff)
The file was modified web/entries/Regex_Equivalence.shtml (diff)
The file was modified web/entries/Regular-Sets.shtml (diff)
The file was modified web/entries/Regular_Algebras.shtml (diff)
The file was modified web/entries/Relation_Algebra.shtml (diff)
The file was modified web/entries/Rep_Fin_Groups.shtml (diff)
The file was modified web/entries/Residuated_Lattices.shtml (diff)
The file was modified web/entries/Ribbon_Proofs.shtml (diff)
The file was modified web/entries/Robbins-Conjecture.shtml (diff)
The file was modified web/entries/Roy_Floyd_Warshall.shtml (diff)
The file was modified web/entries/SATSolverVerification.shtml (diff)
The file was modified web/entries/SIFPL.shtml (diff)
The file was modified web/entries/SIFUM_Type_Systems.shtml (diff)
The file was modified web/entries/Secondary_Sylow.shtml (diff)
The file was modified web/entries/Selection_Heap_Sort.shtml (diff)
The file was modified web/entries/SenSocialChoice.shtml (diff)
The file was modified web/entries/Separation_Algebra.shtml (diff)
The file was modified web/entries/Separation_Logic_Imperative_HOL.shtml (diff)
The file was modified web/entries/SequentInvertibility.shtml (diff)
The file was modified web/entries/Shivers-CFA.shtml (diff)
The file was modified web/entries/ShortestPath.shtml (diff)
The file was modified web/entries/Show.shtml (diff)
The file was modified web/entries/Simpl.shtml (diff)
The file was modified web/entries/Skew_Heap.shtml (diff)
The file was modified web/entries/Slicing.shtml (diff)
The file was modified web/entries/Sort_Encodings.shtml (diff)
The file was modified web/entries/Special_Function_Bounds.shtml (diff)
The file was modified web/entries/Splay_Tree.shtml (diff)
The file was modified web/entries/Sqrt_Babylonian.shtml (diff)
The file was modified web/entries/Statecharts.shtml (diff)
The file was modified web/entries/Stern_Brocot.shtml (diff)
The file was modified web/entries/Stream-Fusion.shtml (diff)
The file was modified web/entries/Stream_Fusion_Code.shtml (diff)
The file was modified web/entries/Strong_Security.shtml (diff)
The file was modified web/entries/Sturm_Sequences.shtml (diff)
The file was modified web/entries/Sturm_Tarski.shtml (diff)
The file was modified web/entries/Stuttering_Equivalence.shtml (diff)
The file was modified web/entries/SumSquares.shtml (diff)
The file was modified web/entries/TLA.shtml (diff)
The file was modified web/entries/Tail_Recursive_Functions.shtml (diff)
The file was modified web/entries/Tarskis_Geometry.shtml (diff)
The file was modified web/entries/Topology.shtml (diff)
The file was modified web/entries/Transitive-Closure-II.shtml (diff)
The file was modified web/entries/Transitive-Closure.shtml (diff)
The file was modified web/entries/Tree-Automata.shtml (diff)
The file was modified web/entries/Triangle.shtml (diff)
The file was modified web/entries/Trie.shtml (diff)
The file was modified web/entries/Tycon.shtml (diff)
The file was modified web/entries/UPF.shtml (diff)
The file was modified web/entries/UpDown_Scheme.shtml (diff)
The file was modified web/entries/Valuation.shtml (diff)
The file was modified web/entries/VectorSpace.shtml (diff)
The file was modified web/entries/Verified-Prover.shtml (diff)
The file was modified web/entries/Vickrey_Clarke_Groves.shtml (diff)
The file was modified web/entries/VolpanoSmith.shtml (diff)
The file was modified web/entries/WHATandWHERE_Security.shtml (diff)
The file was modified web/entries/Well_Quasi_Orders.shtml (diff)
The file was modified web/entries/WorkerWrapper.shtml (diff)
The file was modified web/entries/XML.shtml (diff)
The file was modified web/entries/pGCL.shtml (diff)
Changeset 6445:fd4e47ae27cc by _gerwin.klein@nicta.com.au_:
added missing List_Update entry page
The file was addedweb/entries/List_Update.shtml
Changeset 6444:2d117f79084d by gerwin.klein@nicta.com.au:
import List_Update from afp-devel
The file was addedthys/List_Update/BIT.thy
The file was addedthys/List_Update/BIT_2comp_on2.thy
The file was addedthys/List_Update/BIT_pairwise.thy
The file was addedthys/List_Update/Bit_Strings.thy
The file was addedthys/List_Update/Comb.thy
The file was addedthys/List_Update/Competitive_Analysis.thy
The file was addedthys/List_Update/Inversion.thy
The file was addedthys/List_Update/List_Factoring.thy
The file was addedthys/List_Update/MTF2_Effects.thy
The file was addedthys/List_Update/Move_to_Front.thy
The file was addedthys/List_Update/OPT2.thy
The file was addedthys/List_Update/On_Off.thy
The file was addedthys/List_Update/Partial_Cost_Model.thy
The file was addedthys/List_Update/Phase_Partitioning.thy
The file was addedthys/List_Update/Prob_Theory.thy
The file was addedthys/List_Update/RExp_Var.thy
The file was addedthys/List_Update/ROOT
The file was addedthys/List_Update/Swaps.thy
The file was addedthys/List_Update/TS.thy
The file was addedthys/List_Update/config
The file was addedthys/List_Update/document/root.bib
The file was addedthys/List_Update/document/root.tex
The file was modified metadata/metadata (diff)
The file was modified metadata/topics (diff)
The file was modified thys/Amortized_Complexity/ROOT (diff)
The file was modified thys/ROOTS (diff)
The file was modified web/index.shtml (diff)
The file was modified web/topics.shtml (diff)
The file was removedthys/Amortized_Complexity/BIT.thy
The file was removedthys/Amortized_Complexity/BIT_2comp_on2.thy
The file was removedthys/Amortized_Complexity/BIT_pairwise.thy
The file was removedthys/Amortized_Complexity/Bit_Strings.thy
The file was removedthys/Amortized_Complexity/Comb.thy
The file was removedthys/Amortized_Complexity/Competitive_Analysis.thy
The file was removedthys/Amortized_Complexity/Inversion.thy
The file was removedthys/Amortized_Complexity/List_Factoring.thy
The file was removedthys/Amortized_Complexity/MTF2_Effects.thy
The file was removedthys/Amortized_Complexity/MTF_2comp_on2.thy
The file was removedthys/Amortized_Complexity/MTF_pairwise.thy
The file was removedthys/Amortized_Complexity/Move_to_Front.thy
The file was removedthys/Amortized_Complexity/OPT2.thy
The file was removedthys/Amortized_Complexity/On_Off.thy
The file was removedthys/Amortized_Complexity/Partial_Cost_Model.thy
The file was removedthys/Amortized_Complexity/Phase_Partitioning.thy
The file was removedthys/Amortized_Complexity/Prob_Theory.thy
The file was removedthys/Amortized_Complexity/RExp_Var.thy
The file was removedthys/Amortized_Complexity/Swaps.thy
The file was removedthys/Amortized_Complexity/TS.thy
Changeset 6443:83b6d8d900a1 by gerwin.klein@nicta.com.au:
record 2015 releases, bump Isabelle version to 2016
The file was modified admin/hg-sync (diff)
The file was modified admin/publish (diff)
The file was modified metadata/release-dates (diff)
The file was modified metadata/releases (diff)
Changeset 6442:825295d81b09 by gerwin.klein@nicta.com.au:
website to release mode (afp-2016)
The file was modified metadata/index.tpl (diff)
The file was modified web/entries/Amortized_Complexity.shtml (diff)
The file was modified web/index.shtml (diff)
Changeset 6441:76329be12d4f by haftmann:
unified CHAR with CHR syntax
The file was modified thys/Certification_Monads/Parser_Monad.thy (diff)
The file was modified thys/Containers/Set_Linorder.thy (diff)
The file was modified thys/Isabelle_Meta_Model/Init.thy (diff)
The file was modified thys/Isabelle_Meta_Model/meta_isabelle/Meta_Isabelle.thy (diff)
The file was modified thys/Isabelle_Meta_Model/toy_example/embedding/meta_toy/Parser_META.thy (diff)
The file was modified thys/JinjaThreads/Execute/ToString.thy (diff)
The file was modified thys/Promela/Promela.thy (diff)
The file was modified thys/Show/Old_Datatype/Old_Show.thy (diff)
The file was modified thys/Show/Show.thy (diff)
Changeset 6440:86a99d80d93c by nipkow:
adapted to recent Multiset change
The file was modified thys/Decreasing-Diagrams-II/Decreasing_Diagrams_II.thy (diff)