Changes

Summary

Merged
Fixed incorrect session information & document error
Removed dependency on HOL-Library.RBT_Mapping; removed workaround
Use instances from Show
Merged
Fixed Hidden_Markov_Models
Fixed Monad_Memo_DP
Fixed PTA & removed obsolete lemmas

Changeset 9328:7d27ccf46012 by simon wimmer _wimmers@in.tum.de_: Merged
Changeset 9327:3c081d7981bb by simon wimmer _wimmers@in.tum.de_: Fixed incorrect session information & document error
The file was modified	`thys/Hidden_Markov_Models/ROOT` (diff)
The file was modified	`thys/Monad_Memo_DP/ROOT` (diff)
The file was modified	`thys/Probabilistic_Timed_Automata/library/Graphs.thy` (diff)
Changeset 9326:abe647cd401e by simon wimmer _wimmers@in.tum.de_: Removed dependency on HOL-Library.RBT_Mapping; removed workaround
The file was modified	`thys/Hidden_Markov_Models/HMM_Example.thy` (diff)
The file was modified	`thys/Hidden_Markov_Models/HMM_Implementation.thy` (diff)
The file was modified	`thys/Monad_Memo_DP/example/Bellman_Ford.thy` (diff)
The file was modified	`thys/Monad_Memo_DP/example/CYK.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/example/Min_Ed_Dist0.thy` (diff)
The file was modified	`thys/Monad_Memo_DP/example/OptBST.thy` (diff)
The file was modified	`thys/Monad_Memo_DP/state_monad/Memory.thy` (diff)
The file was removed	`thys/Hidden_Markov_Models/Simple_List_Memory.thy`
Changeset 9325:878f6091860e by simon wimmer _wimmers@in.tum.de_: Use instances from Show
The file was modified	`thys/Monad_Memo_DP/util/Tracing.thy` (diff)
Changeset 9324:51b29b7b53e1 by simon wimmer _wimmers@in.tum.de_: Merged
Changeset 9323:f6a947be4b6a by simon wimmer _wimmers@in.tum.de_: Fixed Hidden_Markov_Models
The file was modified	`thys/Hidden_Markov_Models/Auxiliary.thy` (diff)
The file was modified	`thys/Hidden_Markov_Models/Hidden_Markov_Model.thy` (diff)
Changeset 9322:be7ffc8a6ee7 by simon wimmer _wimmers@in.tum.de_: Fixed Monad_Memo_DP
The file was modified	`thys/Monad_Memo_DP/Index.thy` (diff)
The file was modified	`thys/Monad_Memo_DP/Pure_Monad.thy` (diff)
The file was modified	`thys/Monad_Memo_DP/example/All_Examples.thy` (diff)
The file was modified	`thys/Monad_Memo_DP/example/Bellman_Ford.thy` (diff)
The file was modified	`thys/Monad_Memo_DP/example/CYK.thy` (diff)
The file was modified	`thys/Monad_Memo_DP/example/Counting_Tiles.thy` (diff)
The file was modified	`thys/Monad_Memo_DP/example/Example_Misc.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/example/Min_Ed_Dist0.thy` (diff)
The file was modified	`thys/Monad_Memo_DP/example/OptBST.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_Default.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/Heap_Monad_Ext.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/Pair_Memory.thy` (diff)
The file was modified	`thys/Monad_Memo_DP/heap_monad/State_Heap.thy` (diff)
The file was modified	`thys/Monad_Memo_DP/heap_monad/State_Heap_Misc.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/Memory.thy` (diff)
The file was modified	`thys/Monad_Memo_DP/state_monad/Monad.thy` (diff)
The file was modified	`thys/Monad_Memo_DP/state_monad/State_Main.thy` (diff)
The file was modified	`thys/Monad_Memo_DP/state_monad/State_Monad_Ext.thy` (diff)
The file was modified	`thys/Monad_Memo_DP/transform/Transform.ML` (diff)
The file was modified	`thys/Monad_Memo_DP/transform/Transform_Cmd.thy` (diff)
The file was modified	`thys/Monad_Memo_DP/transform/Transform_Data.ML` (diff)
The file was modified	`thys/Monad_Memo_DP/transform/Transform_Misc.ML` (diff)
The file was modified	`thys/Monad_Memo_DP/transform/Transform_Parser.ML` (diff)
The file was modified	`thys/Monad_Memo_DP/transform/Transform_Tactic.ML` (diff)
The file was modified	`thys/Monad_Memo_DP/util/Ground_Function.ML` (diff)
The file was modified	`thys/Monad_Memo_DP/util/Ground_Function.thy` (diff)
The file was modified	`thys/Monad_Memo_DP/util/Solve_Cong.thy` (diff)
The file was modified	`thys/Monad_Memo_DP/util/Tracing.thy` (diff)
Changeset 9321:dbcb82ac41f4 by simon wimmer _wimmers@in.tum.de_: Fixed PTA & removed obsolete lemmas
The file was modified	`thys/Probabilistic_Timed_Automata/PTA.thy` (diff)
The file was modified	`thys/Probabilistic_Timed_Automata/PTA_Reachability.thy` (diff)
The file was modified	`thys/Probabilistic_Timed_Automata/ROOT` (diff)
The file was modified	`thys/Probabilistic_Timed_Automata/library/Finiteness.thy` (diff)
The file was modified	`thys/Probabilistic_Timed_Automata/library/Graphs.thy` (diff)
The file was modified	`thys/Probabilistic_Timed_Automata/library/Instantiate_Existentials.thy` (diff)
The file was modified	`thys/Probabilistic_Timed_Automata/library/Lib.thy` (diff)
The file was modified	`thys/Probabilistic_Timed_Automata/library/MDP_Aux.thy` (diff)
The file was modified	`thys/Probabilistic_Timed_Automata/library/More_List.thy` (diff)
The file was modified	`thys/Probabilistic_Timed_Automata/library/Sequence.thy` (diff)
The file was modified	`thys/Probabilistic_Timed_Automata/library/Sequence_LTL.thy` (diff)
The file was modified	`thys/Probabilistic_Timed_Automata/library/Stream_More.thy` (diff)