Skip to content
Failed

Changes

Summary

  1. merged
  2. OpSets: adapt to sorted changes
  3. merged
  4. Monad_Memo_DP: update syntax
  5. AxiomaticCategoryTheory: requires smt_oracle = true
  6. AximoaticCategoryTheory: syntax updates
  7. Monad_Memo_DP: Code_Char is gone
  8. merged from afp-2017
  9. Hidden_Markov_Models website
  10. new entry Hidden_Markov_Models
  11. Probabilistic_Timed_Automata webpage
  12. new entry Probabilistic_Timed_Automata
  13. added timeout in ROOT of OpSets
  14. metadata and sitegen for OpSets
  15. new entry: OpSets
  16. New entry AxiomaticCategoryTheory
  17. website for Monad_Memo_DP. Also fixed the ROOT file
  18. new entry Monad_Memo_DP
Changeset 9314:7a5167c92231 by lars hupel _lars.hupel@mytum.de_:
OpSets: adapt to sorted changes
The file was modified thys/OpSets/OpSet.thy (diff)
Changeset 9312:0b0c11957c4e by lars hupel _lars.hupel@mytum.de_:
Monad_Memo_DP: update syntax
The file was modified thys/Monad_Memo_DP/Index.thy (diff)
The file was modified thys/Monad_Memo_DP/example/Counting_Tiles.thy (diff)
The file was modified thys/Monad_Memo_DP/example/Knapsack.thy (diff)
The file was modified thys/Monad_Memo_DP/example/Longest_Common_Subsequence.thy (diff)
The file was modified thys/Monad_Memo_DP/heap_monad/Bottom_Up_Computation_Heap.thy (diff)
The file was modified thys/Monad_Memo_DP/heap_monad/DP_CRelVH.thy (diff)
The file was modified thys/Monad_Memo_DP/heap_monad/DP_CRelVH_Ext.thy (diff)
The file was modified thys/Monad_Memo_DP/heap_monad/Heap_Main.thy (diff)
The file was modified thys/Monad_Memo_DP/heap_monad/Memory_Heap.thy (diff)
The file was modified thys/Monad_Memo_DP/heap_monad/State_Heap.thy (diff)
The file was modified thys/Monad_Memo_DP/state_monad/Bottom_Up_Computation.thy (diff)
The file was modified thys/Monad_Memo_DP/state_monad/DP_CRelVS.thy (diff)
The file was modified thys/Monad_Memo_DP/state_monad/DP_CRelVS_Ext.thy (diff)
The file was modified thys/Monad_Memo_DP/state_monad/State_Main.thy (diff)
Changeset 9311:38fbe84e0ac9 by lars hupel _lars.hupel@mytum.de_:
AxiomaticCategoryTheory: requires smt_oracle = true
The file was modified thys/AxiomaticCategoryTheory/AxiomaticCategoryTheory.thy (diff)
Changeset 9310:47510cd37b1a by lars hupel _lars.hupel@mytum.de_:
AximoaticCategoryTheory: syntax updates
The file was modified thys/AxiomaticCategoryTheory/AxiomaticCategoryTheory.thy (diff)
Changeset 9309:0ec9fb39701a by lars hupel _lars.hupel@mytum.de_:
Monad_Memo_DP: Code_Char is gone
The file was modified thys/Monad_Memo_DP/util/Tracing.thy (diff)
Changeset 9308:e225580affc7 by lars hupel _lars.hupel@mytum.de_:
merged from afp-2017
Changeset 9307:b9060dc1dcf3 by paulson _lp15@cam.ac.uk_:
Hidden_Markov_Models website
The file was addedweb/entries/Hidden_Markov_Models.html
The file was modified metadata/metadata (diff)
The file was modified web/entries/Markov_Models.html (diff)
The file was modified web/entries/Monad_Memo_DP.html (diff)
The file was modified web/index.html (diff)
The file was modified web/rss.xml (diff)
The file was modified web/statistics.html (diff)
The file was modified web/topics.html (diff)
Changeset 9306:a3624ed0e967 by paulson _lp15@cam.ac.uk_:
new entry Hidden_Markov_Models
The file was addedthys/Hidden_Markov_Models/Auxiliary.thy
The file was addedthys/Hidden_Markov_Models/HMM_Example.thy
The file was addedthys/Hidden_Markov_Models/HMM_Implementation.thy
The file was addedthys/Hidden_Markov_Models/Hidden_Markov_Model.thy
The file was addedthys/Hidden_Markov_Models/ROOT
The file was addedthys/Hidden_Markov_Models/Simple_List_Memory.thy
The file was addedthys/Hidden_Markov_Models/document/root.bib
The file was addedthys/Hidden_Markov_Models/document/root.tex
The file was modified thys/ROOTS (diff)
Changeset 9305:9b3b87862b59 by paulson _lp15@cam.ac.uk_:
Probabilistic_Timed_Automata webpage
The file was addedweb/entries/Probabilistic_Timed_Automata.html
The file was modified metadata/metadata (diff)
The file was modified web/entries/Markov_Models.html (diff)
The file was modified web/entries/Timed_Automata.html (diff)
The file was modified web/index.html (diff)
The file was modified web/rss.xml (diff)
The file was modified web/statistics.html (diff)
The file was modified web/topics.html (diff)
Changeset 9304:e62a74f869ab by paulson _lp15@cam.ac.uk_:
new entry Probabilistic_Timed_Automata
The file was addedthys/Probabilistic_Timed_Automata/PTA.thy
The file was addedthys/Probabilistic_Timed_Automata/PTA_Reachability.thy
The file was addedthys/Probabilistic_Timed_Automata/ROOT
The file was addedthys/Probabilistic_Timed_Automata/document/root.bib
The file was addedthys/Probabilistic_Timed_Automata/document/root.tex
The file was addedthys/Probabilistic_Timed_Automata/library/Basic.thy
The file was addedthys/Probabilistic_Timed_Automata/library/Finiteness.thy
The file was addedthys/Probabilistic_Timed_Automata/library/Graphs.thy
The file was addedthys/Probabilistic_Timed_Automata/library/Instantiate_Existentials.thy
The file was addedthys/Probabilistic_Timed_Automata/library/Lib.thy
The file was addedthys/Probabilistic_Timed_Automata/library/MDP_Aux.thy
The file was addedthys/Probabilistic_Timed_Automata/library/More_List.thy
The file was addedthys/Probabilistic_Timed_Automata/library/Sequence.thy
The file was addedthys/Probabilistic_Timed_Automata/library/Sequence_LTL.thy
The file was addedthys/Probabilistic_Timed_Automata/library/Stream_More.thy
The file was modified thys/ROOTS (diff)
Changeset 9303:5f5419263c86 by rene thiemann _rene.thiemann@uibk.ac.at_:
added timeout in ROOT of OpSets
The file was modified thys/OpSets/ROOT (diff)
Changeset 9302:49c015ac2565 by rene thiemann _rene.thiemann@uibk.ac.at_:
metadata and sitegen for OpSets
The file was addedweb/entries/OpSets.html
The file was modified metadata/metadata (diff)
The file was modified web/entries/Algebraic_VCs.html (diff)
The file was modified web/entries/CRDT.html (diff)
The file was modified web/entries/KAD.html (diff)
The file was modified web/entries/KAT_and_DRA.html (diff)
The file was modified web/entries/LambdaMu.html (diff)
The file was modified web/entries/PSemigroupsConvolution.html (diff)
The file was modified web/entries/Residuated_Lattices.html (diff)
The file was modified web/index.html (diff)
The file was modified web/rss.xml (diff)
The file was modified web/statistics.html (diff)
The file was modified web/topics.html (diff)
The file was addedthys/OpSets/Insert_Spec.thy
The file was addedthys/OpSets/Interleaving.thy
The file was addedthys/OpSets/List_Spec.thy
The file was addedthys/OpSets/OpSet.thy
The file was addedthys/OpSets/RGA.thy
The file was addedthys/OpSets/ROOT
The file was addedthys/OpSets/document/root.bib
The file was addedthys/OpSets/document/root.tex
The file was modified thys/ROOTS (diff)
Changeset 9300:f0b3f25f7c6f by nipkow:
New entry AxiomaticCategoryTheory
The file was addedthys/AxiomaticCategoryTheory/AxiomaticCategoryTheory.thy
The file was addedthys/AxiomaticCategoryTheory/ROOT
The file was addedthys/AxiomaticCategoryTheory/document/root.tex
The file was addedweb/entries/AxiomaticCategoryTheory.html
The file was modified metadata/metadata (diff)
The file was modified thys/ROOTS (diff)
The file was modified web/entries/GoedelGod.html (diff)
The file was modified web/entries/Lowe_Ontological_Argument.html (diff)
The file was modified web/entries/Types_Tableaus_and_Goedels_God.html (diff)
The file was modified web/index.html (diff)
The file was modified web/rss.xml (diff)
The file was modified web/statistics.html (diff)
The file was modified web/topics.html (diff)
Changeset 9299:2ee789656686 by paulson _lp15@cam.ac.uk_:
website for Monad_Memo_DP. Also fixed the ROOT file
The file was addedweb/entries/Monad_Memo_DP.html
The file was modified metadata/metadata (diff)
The file was modified thys/Monad_Memo_DP/ROOT (diff)
The file was modified web/index.html (diff)
The file was modified web/rss.xml (diff)
The file was modified web/statistics.html (diff)
The file was modified web/topics.html (diff)
Changeset 9298:91293196287d by paulson _lp15@cam.ac.uk_:
new entry Monad_Memo_DP
The file was addedthys/Monad_Memo_DP/Index.thy
The file was addedthys/Monad_Memo_DP/Pure_Monad.thy
The file was addedthys/Monad_Memo_DP/ROOT
The file was addedthys/Monad_Memo_DP/document/root.bib
The file was addedthys/Monad_Memo_DP/document/root.tex
The file was addedthys/Monad_Memo_DP/example/All_Examples.thy
The file was addedthys/Monad_Memo_DP/example/Bellman_Ford.thy
The file was addedthys/Monad_Memo_DP/example/CYK.thy
The file was addedthys/Monad_Memo_DP/example/Counting_Tiles.thy
The file was addedthys/Monad_Memo_DP/example/Example_Misc.thy
The file was addedthys/Monad_Memo_DP/example/Knapsack.thy
The file was addedthys/Monad_Memo_DP/example/Longest_Common_Subsequence.thy
The file was addedthys/Monad_Memo_DP/example/Min_Ed_Dist0.thy
The file was addedthys/Monad_Memo_DP/example/OptBST.thy
The file was addedthys/Monad_Memo_DP/heap_monad/Bottom_Up_Computation_Heap.thy
The file was addedthys/Monad_Memo_DP/heap_monad/DP_CRelVH.thy
The file was addedthys/Monad_Memo_DP/heap_monad/DP_CRelVH_Ext.thy
The file was addedthys/Monad_Memo_DP/heap_monad/Heap_Default.thy
The file was addedthys/Monad_Memo_DP/heap_monad/Heap_Main.thy
The file was addedthys/Monad_Memo_DP/heap_monad/Heap_Monad_Ext.thy
The file was addedthys/Monad_Memo_DP/heap_monad/Memory_Heap.thy
The file was addedthys/Monad_Memo_DP/heap_monad/Pair_Memory.thy
The file was addedthys/Monad_Memo_DP/heap_monad/State_Heap.thy
The file was addedthys/Monad_Memo_DP/heap_monad/State_Heap_Misc.thy
The file was addedthys/Monad_Memo_DP/state_monad/Bottom_Up_Computation.thy
The file was addedthys/Monad_Memo_DP/state_monad/DP_CRelVS.thy
The file was addedthys/Monad_Memo_DP/state_monad/DP_CRelVS_Ext.thy
The file was addedthys/Monad_Memo_DP/state_monad/Memory.thy
The file was addedthys/Monad_Memo_DP/state_monad/Monad.thy
The file was addedthys/Monad_Memo_DP/state_monad/State_Main.thy
The file was addedthys/Monad_Memo_DP/state_monad/State_Monad_Ext.thy
The file was addedthys/Monad_Memo_DP/transform/Transform.ML
The file was addedthys/Monad_Memo_DP/transform/Transform_Cmd.thy
The file was addedthys/Monad_Memo_DP/transform/Transform_Const.ML
The file was addedthys/Monad_Memo_DP/transform/Transform_Data.ML
The file was addedthys/Monad_Memo_DP/transform/Transform_Misc.ML
The file was addedthys/Monad_Memo_DP/transform/Transform_Parser.ML
The file was addedthys/Monad_Memo_DP/transform/Transform_Tactic.ML
The file was addedthys/Monad_Memo_DP/transform/Transform_Term.ML
The file was addedthys/Monad_Memo_DP/util/Ground_Function.ML
The file was addedthys/Monad_Memo_DP/util/Ground_Function.thy
The file was addedthys/Monad_Memo_DP/util/Solve_Cong.thy
The file was addedthys/Monad_Memo_DP/util/Tracing.thy
The file was modified thys/ROOTS (diff)