Skip to content
Success

Changes

Summary

  1. merged
  2. split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
  3. proper name mangling of "undefined" constants in Sledgehammer
  4. earlier availability of lifting
  5. more correct transfer
  6. merged
  7. proper abstraction of function variables when instantiating induction rules in Sledgehammer
  8. added lemma asympD
  9. added lemma
  10. Some lemmas about continuous functions with integral zero
Changeset 74982:a10873b3c7d4 by desharna:
merged
Changeset 74981:10df7a627ab6 by desharna:
split option "sledgehammer_atp_dest_dir" into "sledgehammer_atp_prob_dest_dir" and "sledgehammer_atp_proof_dest_dir"
The file was modified NEWS
The file was modified src/Doc/Sledgehammer/document/root.tex
The file was modified src/HOL/TPTP/mash_eval.ML
The file was modified src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
Changeset 74980:8dd527e97ddb by desharna:
proper name mangling of "undefined" constants in Sledgehammer
The file was modified src/HOL/Tools/ATP/atp_problem_generate.ML
Changeset 74979:4d77dd3019d1 by haftmann:
earlier availability of lifting
The file was modified src/HOL/Equiv_Relations.thy
The file was modified src/HOL/Groups_Big.thy
The file was modified src/HOL/Int.thy
The file was modified src/HOL/Lattices_Big.thy
The file was modified src/HOL/Lifting_Set.thy
Changeset 74978:1f30aa91f496 by haftmann:
more correct transfer
The file was modified src/Pure/Isar/code.ML
Changeset 74977:e4fd3989554d by desharna:
merged
Changeset 74976:70aab133dc8d by desharna:
proper abstraction of function variables when instantiating induction rules in Sledgehammer
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
Changeset 74975:5d3a846bccf8 by desharna:
added lemma asympD
The file was modified src/HOL/Relation.thy
Changeset 74974:7733c794cfea by nipkow:
added lemma
The file was modified src/HOL/Library/While_Combinator.thy
Changeset 74973:a565a2889b49 by paulson _lp15@cam.ac.uk_:
Some lemmas about continuous functions with integral zero
The file was modified src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy

Summary

  1. Tuning.
  2. merged
  3. tweaks
  4. merged
  5. Fixed an inadequate description
  6. tuned
  7. mv to distribution
  8. by now in distribution
  9. merge from afp-2021-1
  10. fixed abstract
  11. tuned
  12. website and metadata for Hyperdual
  13. new entry: Hyperdual
  14. sorted ROOTS
  15. tuned
  16. New entry Knights_Tour
  17. more thoroughly replace Michael Foster's e-mail address
  18. metadata and sitegen for Gale_Shapley
  19. new entry Gale_Shapley
  20. update Michael Forster's email address
  21. metadata and sitegen for Roth_Arithmetic_Progressions
  22. new entry Roth_Arithmetic_Progressions
  23. typo
  24. merged
  25. New entry Regular_Tree_Relations
  26. We DON'T want an output directory
  27. MDP-Algorithms website
  28. new entry MDP-Algorithms
  29. typo
  30. new entry MDP-Rewards
  31. fixed typo
The file was modified thys/Bicategory/Bicategory.thy
The file was modified thys/Bicategory/BicategoryOfSpans.thy
The file was modified thys/Bicategory/Coherence.thy
The file was modified thys/Bicategory/Prebicategory.thy
The file was modified thys/Bicategory/Pseudofunctor.thy
The file was modified thys/Bicategory/SpanBicategory.thy
The file was modified thys/Bicategory/Subbicategory.thy
The file was modified thys/Category3/Adjunction.thy
Changeset 12360:6772d0f44fcd by paulson:
merged
The file was modified thys/Nash_Williams/Nash_Williams.thy
Changeset 12358:e1da0b0d0794 by paulson:
merged
Changeset 12357:b34d91e2ee32 by paulson _lp15@cam.ac.uk_:
Fixed an inadequate description
The file was modified thys/Special_Function_Bounds/ROOT
Changeset 12356:d858bca8a11d by haftmann:
tuned
The file was modified thys/Nested_Multisets_Ordinals/Multiset_More.thy
Changeset 12355:20e68f30d833 by nipkow:
mv to distribution
The file was modified thys/Gale_Shapley/Gale_Shapley1.thy
Changeset 12354:1e6800ff5ef5 by nipkow:
by now in distribution
The file was modified thys/Gale_Shapley/Gale_Shapley1.thy
Changeset 12353:bcab7766727b by gerwin klein _kleing@unsw.edu.au_:
merge from afp-2021-1
Changeset 12352:af1ef62a1c06 by nipkow:
fixed abstract
The file was modified web/entries/Knights_Tour.html
The file was modified web/rss.xml
The file was modified web/statistics.html
Changeset 12351:ca0d59395b21 by nipkow:
tuned
The file was modified metadata/metadata
Changeset 12350:581f20291792 by rene thiemann _rene.thiemann@uibk.ac.at_:
website and metadata for Hyperdual
The file was addedweb/entries/Hyperdual.html
The file was modified metadata/metadata
The file was modified web/index.html
The file was modified web/rss.xml
The file was modified web/statistics.html
The file was modified web/topics.html
The file was addedthys/Hyperdual/AnalyticTestFunction.thy
The file was addedthys/Hyperdual/Hyperdual.thy
The file was addedthys/Hyperdual/HyperdualFunctionExtension.thy
The file was addedthys/Hyperdual/LogisticFunction.thy
The file was addedthys/Hyperdual/ROOT
The file was addedthys/Hyperdual/TwiceFieldDifferentiable.thy
The file was addedthys/Hyperdual/document/root.bib
The file was addedthys/Hyperdual/document/root.tex
The file was modified thys/ROOTS
The file was modified thys/ROOTS
Changeset 12347:aee6164bd5e8 by nipkow:
tuned
The file was modified thys/Gale_Shapley/document/root.tex
Changeset 12346:53adb4f2af3d by nipkow:
New entry Knights_Tour
The file was addedthys/Knights_Tour/KnightsTour.thy
The file was addedthys/Knights_Tour/ROOT
The file was addedthys/Knights_Tour/document/root.bib
The file was addedthys/Knights_Tour/document/root.tex
The file was addedweb/entries/Knights_Tour.html
The file was modified metadata/metadata
The file was modified thys/ROOTS
The file was modified web/index.html
The file was modified web/rss.xml
The file was modified web/statistics.html
The file was modified web/topics.html
Changeset 12345:19a4643c4a5d by andreas lochbihler _mail@andreas-lochbihler.de_:
more thoroughly replace Michael Foster's e-mail address
The file was modified metadata/metadata
Changeset 12344:f48cffadd15d by andreas lochbihler _mail@andreas-lochbihler.de_:
metadata and sitegen for Gale_Shapley
The file was addedweb/entries/Gale_Shapley.html
The file was modified metadata/metadata
The file was modified thys/Gale_Shapley/ROOT
The file was modified web/entries/Collections.html
The file was modified web/entries/List-Index.html
The file was modified web/index.html
The file was modified web/rss.xml
The file was modified web/statistics.html
The file was modified web/topics.html
The file was addedthys/Gale_Shapley/Gale_Shapley1.thy
The file was addedthys/Gale_Shapley/Gale_Shapley2.thy
The file was addedthys/Gale_Shapley/ROOT
The file was addedthys/Gale_Shapley/document/root.bib
The file was addedthys/Gale_Shapley/document/root.tex
The file was modified thys/ROOTS
Changeset 12342:6f3ebcaf3949 by andreas lochbihler _mail@andreas-lochbihler.de_:
update Michael Forster's email address
The file was modified metadata/metadata
The file was modified web/entries/Extended_Finite_State_Machine_Inference.html
The file was modified web/entries/Extended_Finite_State_Machines.html
Changeset 12341:32852fd86914 by andreas lochbihler _mail@andreas-lochbihler.de_:
metadata and sitegen for Roth_Arithmetic_Progressions
The file was addedweb/entries/Roth_Arithmetic_Progressions.html
The file was modified metadata/metadata
The file was modified web/entries/Amicable_Numbers.html
The file was modified web/entries/Aristotles_Assertoric_Syllogistic.html
The file was modified web/entries/Ergodic_Theory.html
The file was modified web/entries/Girth_Chromatic.html
The file was modified web/entries/Irrational_Series_Erdos_Straus.html
The file was modified web/entries/Irrationality_J_Hancl.html
The file was modified web/entries/Octonions.html
The file was modified web/entries/Random_Graph_Subgraph_Threshold.html
The file was modified web/entries/Szemeredi_Regularity.html
The file was modified web/entries/Transcendence_Series_Hancl_Rucki.html
The file was modified web/index.html
The file was modified web/rss.xml
The file was modified web/statistics.html
The file was modified web/topics.html
Changeset 12340:60e74aa9562c by andreas lochbihler _mail@andreas-lochbihler.de_:
new entry Roth_Arithmetic_Progressions
The file was addedthys/Roth_Arithmetic_Progressions/ROOT
The file was addedthys/Roth_Arithmetic_Progressions/Roth_Arithmetic_Progressions.thy
The file was addedthys/Roth_Arithmetic_Progressions/document/root.tex
The file was modified thys/ROOTS
Changeset 12339:2cc9c652d3fd by nipkow:
typo
The file was modified metadata/README
Changeset 12338:d6111a80ce2a by nipkow:
merged
Changeset 12337:6a4f3c47c3d8 by nipkow:
New entry Regular_Tree_Relations
The file was addedthys/Regular_Tree_Relations/AGTT.thy
The file was addedthys/Regular_Tree_Relations/GTT.thy
The file was addedthys/Regular_Tree_Relations/GTT_Compose.thy
The file was addedthys/Regular_Tree_Relations/GTT_Transitive_Closure.thy
The file was addedthys/Regular_Tree_Relations/Horn_Setup/Horn_Fset.thy
The file was addedthys/Regular_Tree_Relations/Horn_Setup/Horn_Inference.thy
The file was addedthys/Regular_Tree_Relations/Horn_Setup/Horn_List.thy
The file was addedthys/Regular_Tree_Relations/Pair_Automaton.thy
The file was addedthys/Regular_Tree_Relations/ROOT
The file was addedthys/Regular_Tree_Relations/RR2_Infinite.thy
The file was addedthys/Regular_Tree_Relations/RR2_Infinite_Q_infinity.thy
The file was addedthys/Regular_Tree_Relations/RRn_Automata.thy
The file was addedthys/Regular_Tree_Relations/Regular_Relation_Abstract_Impl.thy
The file was addedthys/Regular_Tree_Relations/Regular_Relation_Impl.thy
The file was addedthys/Regular_Tree_Relations/Tree_Automata/Myhill_Nerode.thy
The file was addedthys/Regular_Tree_Relations/Tree_Automata/Tree_Automata.thy
The file was addedthys/Regular_Tree_Relations/Tree_Automata/Tree_Automata_Abstract_Impl.thy
The file was addedthys/Regular_Tree_Relations/Tree_Automata/Tree_Automata_Class_Instances_Impl.thy
The file was addedthys/Regular_Tree_Relations/Tree_Automata/Tree_Automata_Complement.thy
The file was addedthys/Regular_Tree_Relations/Tree_Automata/Tree_Automata_Det.thy
The file was addedthys/Regular_Tree_Relations/Tree_Automata/Tree_Automata_Impl.thy
The file was addedthys/Regular_Tree_Relations/Tree_Automata/Tree_Automata_Pumping.thy
The file was addedthys/Regular_Tree_Relations/Util/Basic_Utils.thy
The file was addedthys/Regular_Tree_Relations/Util/FSet_Utils.thy
The file was addedthys/Regular_Tree_Relations/Util/Ground_Closure.thy
The file was addedthys/Regular_Tree_Relations/Util/Ground_Ctxt.thy
The file was addedthys/Regular_Tree_Relations/Util/Ground_Terms.thy
The file was addedthys/Regular_Tree_Relations/Util/Term_Context.thy
The file was addedthys/Regular_Tree_Relations/document/root.bib
The file was addedthys/Regular_Tree_Relations/document/root.tex
The file was addedweb/entries/Regular_Tree_Relations.html
The file was modified metadata/metadata
The file was modified thys/ROOTS
The file was modified web/entries/Abstract-Rewriting.html
The file was modified web/entries/Algebraic_Numbers.html
The file was modified web/entries/Berlekamp_Zassenhaus.html
The file was modified web/entries/Certification_Monads.html
The file was modified web/entries/Cubic_Quartic_Equations.html
The file was modified web/entries/Datatype_Order_Generator.html
The file was modified web/entries/Decreasing-Diagrams-II.html
The file was modified web/entries/Deriving.html
The file was modified web/entries/Diophantine_Eqns_Lin_Hom.html
The file was modified web/entries/Efficient-Mergesort.html
The file was modified web/entries/Factor_Algebraic_Polynomial.html
The file was modified web/entries/Farkas.html
The file was modified web/entries/First_Order_Terms.html
The file was modified web/entries/Goodstein_Lambda.html
The file was modified web/entries/HOLCF-Prelude.html
The file was modified web/entries/Imperative_Insertion_Sort.html
The file was modified web/entries/Jordan_Normal_Form.html
The file was modified web/entries/Knuth_Bendix_Order.html
The file was modified web/entries/LLL_Basis_Reduction.html
The file was modified web/entries/LLL_Factorization.html
The file was modified web/entries/Lifting_Definition_Option.html
The file was modified web/entries/Linear_Inequalities.html
The file was modified web/entries/Matrix.html
The file was modified web/entries/Minsky_Machines.html
The file was modified web/entries/Modular_arithmetic_LLL_and_HNF_algorithms.html
The file was modified web/entries/Open_Induction.html
The file was modified web/entries/Partial_Function_MR.html
The file was modified web/entries/Perron_Frobenius.html
The file was modified web/entries/Polynomial_Factorization.html
The file was modified web/entries/Polynomial_Interpolation.html
The file was modified web/entries/Polynomials.html
The file was modified web/entries/Real_Impl.html
The file was modified web/entries/Rewriting_Z.html
The file was modified web/entries/Show.html
The file was modified web/entries/Simplex.html
The file was modified web/entries/Sqrt_Babylonian.html
The file was modified web/entries/Stochastic_Matrices.html
The file was modified web/entries/Subresultants.html
The file was modified web/entries/Sunflowers.html
The file was modified web/entries/Transitive-Closure-II.html
The file was modified web/entries/Transitive-Closure.html
The file was modified web/entries/Weighted_Path_Order.html
The file was modified web/entries/Well_Quasi_Orders.html
The file was modified web/entries/XML.html
The file was modified web/index.html
The file was modified web/rss.xml
The file was modified web/statistics.html
The file was modified web/topics.html
Changeset 12336:e7ccade6ae5d by paulson _lp15@cam.ac.uk_:
We DON'T want an output directory
The file was modified thys/MDP-Algorithms/ROOT
The file was removedthys/MDP-Algorithms/output/document.pdf
The file was removedthys/MDP-Algorithms/output/document/Algorithms.tex
The file was removedthys/MDP-Algorithms/output/document/Blinfun_Matrix.tex
The file was removedthys/MDP-Algorithms/output/document/Code_DP.tex
The file was removedthys/MDP-Algorithms/output/document/Code_Gridworld.tex
The file was removedthys/MDP-Algorithms/output/document/Code_Inventory.tex
The file was removedthys/MDP-Algorithms/output/document/Code_Mod.tex
The file was removedthys/MDP-Algorithms/output/document/Code_Real_Approx_By_Float_Fix.tex
The file was removedthys/MDP-Algorithms/output/document/Examples.tex
The file was removedthys/MDP-Algorithms/output/document/Matrix_Util.tex
The file was removedthys/MDP-Algorithms/output/document/Modified_Policy_Iteration.tex
The file was removedthys/MDP-Algorithms/output/document/Policy_Iteration.tex
The file was removedthys/MDP-Algorithms/output/document/Splitting_Methods.tex
The file was removedthys/MDP-Algorithms/output/document/Value_Iteration.tex
The file was removedthys/MDP-Algorithms/output/document/comment.sty
The file was removedthys/MDP-Algorithms/output/document/isabelle.sty
The file was removedthys/MDP-Algorithms/output/document/isabellesym.sty
The file was removedthys/MDP-Algorithms/output/document/isabelletags.sty
The file was removedthys/MDP-Algorithms/output/document/pdfsetup.sty
The file was removedthys/MDP-Algorithms/output/document/railsetup.sty
The file was removedthys/MDP-Algorithms/output/document/root.bib
The file was removedthys/MDP-Algorithms/output/document/root.tex
The file was removedthys/MDP-Algorithms/output/document/session.tex
The file was removedthys/MDP-Algorithms/output/document/session_graph.pdf
The file was removedthys/MDP-Algorithms/output/outline.pdf
The file was removedthys/MDP-Algorithms/output/outline/Algorithms.tex
The file was removedthys/MDP-Algorithms/output/outline/Blinfun_Matrix.tex
The file was removedthys/MDP-Algorithms/output/outline/Code_DP.tex
The file was removedthys/MDP-Algorithms/output/outline/Code_Gridworld.tex
The file was removedthys/MDP-Algorithms/output/outline/Code_Inventory.tex
The file was removedthys/MDP-Algorithms/output/outline/Code_Mod.tex
The file was removedthys/MDP-Algorithms/output/outline/Code_Real_Approx_By_Float_Fix.tex
The file was removedthys/MDP-Algorithms/output/outline/Examples.tex
The file was removedthys/MDP-Algorithms/output/outline/Matrix_Util.tex
The file was removedthys/MDP-Algorithms/output/outline/Modified_Policy_Iteration.tex
The file was removedthys/MDP-Algorithms/output/outline/Policy_Iteration.tex
The file was removedthys/MDP-Algorithms/output/outline/Splitting_Methods.tex
The file was removedthys/MDP-Algorithms/output/outline/Value_Iteration.tex
The file was removedthys/MDP-Algorithms/output/outline/comment.sty
The file was removedthys/MDP-Algorithms/output/outline/isabelle.sty
The file was removedthys/MDP-Algorithms/output/outline/isabellesym.sty
The file was removedthys/MDP-Algorithms/output/outline/isabelletags.sty
The file was removedthys/MDP-Algorithms/output/outline/pdfsetup.sty
The file was removedthys/MDP-Algorithms/output/outline/railsetup.sty
The file was removedthys/MDP-Algorithms/output/outline/root.bib
The file was removedthys/MDP-Algorithms/output/outline/root.tex
The file was removedthys/MDP-Algorithms/output/outline/session.tex
The file was removedthys/MDP-Algorithms/output/outline/session_graph.pdf
Changeset 12335:d5b7918837dc by paulson _lp15@cam.ac.uk_:
MDP-Algorithms website
The file was addedweb/entries/MDP-Algorithms.html
The file was modified metadata/metadata
The file was modified web/entries/Gauss_Jordan.html
The file was modified web/entries/MDP-Rewards.html
The file was modified web/index.html
The file was modified web/rss.xml
The file was modified web/statistics.html
The file was modified web/topics.html
Changeset 12334:c5c46dda8d59 by paulson _lp15@cam.ac.uk_:
new entry MDP-Algorithms
The file was addedthys/MDP-Algorithms/Algorithms.thy
The file was addedthys/MDP-Algorithms/Blinfun_Matrix.thy
The file was addedthys/MDP-Algorithms/Matrix_Util.thy
The file was addedthys/MDP-Algorithms/Modified_Policy_Iteration.thy
The file was addedthys/MDP-Algorithms/Policy_Iteration.thy
The file was addedthys/MDP-Algorithms/ROOT
The file was addedthys/MDP-Algorithms/Splitting_Methods.thy
The file was addedthys/MDP-Algorithms/Value_Iteration.thy
The file was addedthys/MDP-Algorithms/code/Code_DP.thy
The file was addedthys/MDP-Algorithms/code/Code_Mod.thy
The file was addedthys/MDP-Algorithms/code/Code_Real_Approx_By_Float_Fix.thy
The file was addedthys/MDP-Algorithms/document/root.bib
The file was addedthys/MDP-Algorithms/document/root.tex
The file was addedthys/MDP-Algorithms/examples/Code_Gridworld.thy
The file was addedthys/MDP-Algorithms/examples/Code_Inventory.thy
The file was addedthys/MDP-Algorithms/examples/Examples.thy
The file was addedthys/MDP-Algorithms/output/document.pdf
The file was addedthys/MDP-Algorithms/output/document/Algorithms.tex
The file was addedthys/MDP-Algorithms/output/document/Blinfun_Matrix.tex
The file was addedthys/MDP-Algorithms/output/document/Code_DP.tex
The file was addedthys/MDP-Algorithms/output/document/Code_Gridworld.tex
The file was addedthys/MDP-Algorithms/output/document/Code_Inventory.tex
The file was addedthys/MDP-Algorithms/output/document/Code_Mod.tex
The file was addedthys/MDP-Algorithms/output/document/Code_Real_Approx_By_Float_Fix.tex
The file was addedthys/MDP-Algorithms/output/document/Examples.tex
The file was addedthys/MDP-Algorithms/output/document/Matrix_Util.tex
The file was addedthys/MDP-Algorithms/output/document/Modified_Policy_Iteration.tex
The file was addedthys/MDP-Algorithms/output/document/Policy_Iteration.tex
The file was addedthys/MDP-Algorithms/output/document/Splitting_Methods.tex
The file was addedthys/MDP-Algorithms/output/document/Value_Iteration.tex
The file was addedthys/MDP-Algorithms/output/document/comment.sty
The file was addedthys/MDP-Algorithms/output/document/isabelle.sty
The file was addedthys/MDP-Algorithms/output/document/isabellesym.sty
The file was addedthys/MDP-Algorithms/output/document/isabelletags.sty
The file was addedthys/MDP-Algorithms/output/document/pdfsetup.sty
The file was addedthys/MDP-Algorithms/output/document/railsetup.sty
The file was addedthys/MDP-Algorithms/output/document/root.bib
The file was addedthys/MDP-Algorithms/output/document/root.tex
The file was addedthys/MDP-Algorithms/output/document/session.tex
The file was addedthys/MDP-Algorithms/output/document/session_graph.pdf
The file was addedthys/MDP-Algorithms/output/outline.pdf
The file was addedthys/MDP-Algorithms/output/outline/Algorithms.tex
The file was addedthys/MDP-Algorithms/output/outline/Blinfun_Matrix.tex
The file was addedthys/MDP-Algorithms/output/outline/Code_DP.tex
The file was addedthys/MDP-Algorithms/output/outline/Code_Gridworld.tex
The file was addedthys/MDP-Algorithms/output/outline/Code_Inventory.tex
The file was addedthys/MDP-Algorithms/output/outline/Code_Mod.tex
The file was addedthys/MDP-Algorithms/output/outline/Code_Real_Approx_By_Float_Fix.tex
The file was addedthys/MDP-Algorithms/output/outline/Examples.tex
The file was addedthys/MDP-Algorithms/output/outline/Matrix_Util.tex
The file was addedthys/MDP-Algorithms/output/outline/Modified_Policy_Iteration.tex
The file was addedthys/MDP-Algorithms/output/outline/Policy_Iteration.tex
The file was addedthys/MDP-Algorithms/output/outline/Splitting_Methods.tex
The file was addedthys/MDP-Algorithms/output/outline/Value_Iteration.tex
The file was addedthys/MDP-Algorithms/output/outline/comment.sty
The file was addedthys/MDP-Algorithms/output/outline/isabelle.sty
The file was addedthys/MDP-Algorithms/output/outline/isabellesym.sty
The file was addedthys/MDP-Algorithms/output/outline/isabelletags.sty
The file was addedthys/MDP-Algorithms/output/outline/pdfsetup.sty
The file was addedthys/MDP-Algorithms/output/outline/railsetup.sty
The file was addedthys/MDP-Algorithms/output/outline/root.bib
The file was addedthys/MDP-Algorithms/output/outline/root.tex
The file was addedthys/MDP-Algorithms/output/outline/session.tex
The file was addedthys/MDP-Algorithms/output/outline/session_graph.pdf
The file was modified thys/ROOTS
The file was modified web/entries/Szemeredi_Regularity.html
Changeset 12332:4b98c55b4f7f by paulson _lp15@cam.ac.uk_:
new entry MDP-Rewards
The file was addedthys/MDP-Rewards/Blinfun_Util.thy
The file was addedthys/MDP-Rewards/Bounded_Functions.thy
The file was addedthys/MDP-Rewards/MDP_cont.thy
The file was addedthys/MDP-Rewards/MDP_disc.thy
The file was addedthys/MDP-Rewards/MDP_reward.thy
The file was addedthys/MDP-Rewards/MDP_reward_Util.thy
The file was addedthys/MDP-Rewards/ROOT
The file was addedthys/MDP-Rewards/document/root.bib
The file was addedthys/MDP-Rewards/document/root.tex
The file was addedweb/entries/MDP-Rewards.html
The file was modified metadata/metadata
The file was modified thys/ROOTS
The file was modified web/index.html
The file was modified web/rss.xml
The file was modified web/statistics.html
The file was modified web/topics.html
Changeset 12331:1f4297082cc1 by paulson _lp15@cam.ac.uk_:
fixed typo
The file was modified metadata/metadata