Skip to content
Success

Changes

Summary

  1. merged, resolving trivial conflict in thys/Markov_Models/Classifying_Markov_Chain_States.thy;
  2. more accurate timeout;
  3. eliminated old 'def' command;
  4. tuned whitespace;
Changeset 8577:b04b4ea69e8c by wenzelm:
merged, resolving trivial conflict in thys/Markov_Models/Classifying_Markov_Chain_States.thy;
Changeset 8576:a9a445faaf8b by wenzelm:
more accurate timeout;
The file was modified thys/Deep_Learning/ROOT (diff)
Changeset 8575:4c491ab73889 by wenzelm:
eliminated old 'def' command;
The file was modified thys/Automatic_Refinement/Lib/Misc.thy (diff)
The file was modified thys/CAVA_Automata/Automata.thy (diff)
The file was modified thys/CAVA_Automata/Simulation.thy (diff)
The file was modified thys/CAVA_LTL_Modelchecker/Nested_DFS/NDFS_SI.thy (diff)
The file was modified thys/Collections/Examples/Autoref/Nested_DFS.thy (diff)
The file was modified thys/Collections/GenCF/Impl/Impl_Array_Hash_Map.thy (diff)
The file was modified thys/Collections/ICF/gen_algo/ListGA.thy (diff)
The file was modified thys/Collections/ICF/gen_algo/MapGA.thy (diff)
The file was modified thys/Collections/ICF/impl/ArrayMapImpl.thy (diff)
The file was modified thys/Collections/ICF/impl/TrieMapImpl.thy (diff)
The file was modified thys/Collections/ICF/impl/Trie_Impl.thy (diff)
The file was modified thys/Collections/Iterator/SetIteratorGA.thy (diff)
The file was modified thys/Collections/Iterator/SetIteratorOperations.thy (diff)
The file was modified thys/Collections/Lib/Diff_Array.thy (diff)
The file was modified thys/Collections/Lib/Robdd.thy (diff)
The file was modified thys/Completeness/PermutationLemmas.thy (diff)
The file was modified thys/Consensus_Refined/MRU/CT_Proofs.thy (diff)
The file was modified thys/Consensus_Refined/MRU/New_Algorithm_Proofs.thy (diff)
The file was modified thys/Consensus_Refined/MRU/Paxos_Proofs.thy (diff)
The file was modified thys/Consensus_Refined/MRU/Three_Step_MRU.thy (diff)
The file was modified thys/Consensus_Refined/MRU/Two_Step_MRU.thy (diff)
The file was modified thys/Consensus_Refined/Observing/BenOr_Proofs.thy (diff)
The file was modified thys/Consensus_Refined/Observing/Two_Step_Observing.thy (diff)
The file was modified thys/Consensus_Refined/Observing/Uv_Proofs.thy (diff)
The file was modified thys/Consensus_Refined/Voting.thy (diff)
The file was modified thys/Consensus_Refined/Voting/Ate_Proofs.thy (diff)
The file was modified thys/Consensus_Refined/Voting/OneThirdRule_Proofs.thy (diff)
The file was modified thys/Containers/Extend_Partial_Order.thy (diff)
The file was modified thys/Containers/Set_Linorder.thy (diff)
The file was modified thys/CryptHOL/GPV_Bisim.thy (diff)
The file was modified thys/CryptHOL/Generative_Probabilistic_Value.thy (diff)
The file was modified thys/DFS_Framework/Examples/DFS_Find_Path.thy (diff)
The file was modified thys/DFS_Framework/Examples/Nested_DFS.thy (diff)
The file was modified thys/DFS_Framework/Examples/Reachable_Nodes.thy (diff)
The file was modified thys/DFS_Framework/Examples/Tarjan.thy (diff)
The file was modified thys/DFS_Framework/Examples/Tarjan_LowLink.thy (diff)
The file was modified thys/Deep_Learning/DL_Deep_Model.thy (diff)
The file was modified thys/Deep_Learning/DL_Network.thy (diff)
The file was modified thys/Deep_Learning/DL_Rank_CP_Rank.thy (diff)
The file was modified thys/Deep_Learning/DL_Shallow_Model.thy (diff)
The file was modified thys/Deep_Learning/Lebesgue_Zero_Set.thy (diff)
The file was modified thys/Deep_Learning/PP_MPoly.thy (diff)
The file was modified thys/Deep_Learning/PP_More_List2.thy (diff)
The file was modified thys/Deep_Learning/PP_More_MPoly.thy (diff)
The file was modified thys/Deep_Learning/PP_Poly_Mapping.thy (diff)
The file was modified thys/Deep_Learning/PP_Univariate.thy (diff)
The file was modified thys/Deep_Learning/Tensor_Product.thy (diff)
The file was modified thys/Deep_Learning/Tensor_Rank.thy (diff)
The file was modified thys/Dependent_SIFUM_Refinement/CompositionalRefinement.thy (diff)
The file was modified thys/Dependent_SIFUM_Type_Systems/Compositionality.thy (diff)
The file was modified thys/Dependent_SIFUM_Type_Systems/LocallySoundModeUse.thy (diff)
The file was modified thys/Dependent_SIFUM_Type_Systems/TypeSystem.thy (diff)
The file was modified thys/Echelon_Form/Echelon_Form.thy (diff)
The file was modified thys/Echelon_Form/Rings2.thy (diff)
The file was modified thys/Encodability_Process_Calculi/CombinedCriteria.thy (diff)
The file was modified thys/Encodability_Process_Calculi/FullAbstraction.thy (diff)
The file was modified thys/Encodability_Process_Calculi/OperationalCorrespondence.thy (diff)
The file was modified thys/FLP/AsynchronousSystem.thy (diff)
The file was modified thys/FLP/Execution.thy (diff)
The file was modified thys/FLP/FLPSystem.thy (diff)
The file was modified thys/FLP/FLPTheorem.thy (diff)
The file was modified thys/FLP/ListUtilities.thy (diff)
The file was modified thys/Flyspeck-Tame/EnumeratorProps.thy (diff)
The file was modified thys/Flyspeck-Tame/FaceDivisionProps.thy (diff)
The file was modified thys/Flyspeck-Tame/GraphProps.thy (diff)
The file was modified thys/Flyspeck-Tame/Invariants.thy (diff)
The file was modified thys/Flyspeck-Tame/ListAux.thy (diff)
The file was modified thys/Flyspeck-Tame/LowerBound.thy (diff)
The file was modified thys/Flyspeck-Tame/Rotation.thy (diff)
The file was modified thys/Formula_Derivatives/Presburger_Formula.thy (diff)
The file was modified thys/Formula_Derivatives/WS1S_Alt_Formula.thy (diff)
The file was modified thys/Formula_Derivatives/WS1S_Formula.thy (diff)
The file was modified thys/Formula_Derivatives/While_Default.thy (diff)
The file was modified thys/Free-Groups/Isomorphisms.thy (diff)
The file was modified thys/Free-Groups/PingPongLemma.thy (diff)
The file was modified thys/Gabow_SCC/Find_Path_Impl.thy (diff)
The file was modified thys/Gabow_SCC/Gabow_GBG.thy (diff)
The file was modified thys/Gabow_SCC/Gabow_Skeleton.thy (diff)
The file was modified thys/Game_Based_Crypto/Guessing_Many_One.thy (diff)
The file was modified thys/Game_Based_Crypto/Hashed_Elgamal.thy (diff)
The file was modified thys/Game_Based_Crypto/PRF_IND_CPA.thy (diff)
The file was modified thys/Game_Based_Crypto/PRF_UHF.thy (diff)
The file was modified thys/Game_Based_Crypto/PRF_UPF_IND_CCA.thy (diff)
The file was modified thys/Gauss_Jordan/Determinants2.thy (diff)
The file was modified thys/Gauss_Jordan/Determinants_IArrays.thy (diff)
The file was modified thys/Gauss_Jordan/Gauss_Jordan.thy (diff)
The file was modified thys/Gauss_Jordan/Gauss_Jordan_IArrays.thy (diff)
The file was modified thys/Gauss_Jordan/Gauss_Jordan_PA.thy (diff)
The file was modified thys/Gauss_Jordan/Gauss_Jordan_PA_IArrays.thy (diff)
The file was modified thys/Gauss_Jordan/Linear_Maps.thy (diff)
The file was modified thys/Gauss_Jordan/System_Of_Equations.thy (diff)
The file was modified thys/Gauss_Jordan/System_Of_Equations_IArrays.thy (diff)
The file was modified thys/Girth_Chromatic/Girth_Chromatic.thy (diff)
The file was modified thys/Graph_Theory/Arc_Walk.thy (diff)
The file was modified thys/Graph_Theory/Digraph_Component.thy (diff)
The file was modified thys/Graph_Theory/Digraph_Isomorphism.thy (diff)
The file was modified thys/Graph_Theory/Euler.thy (diff)
The file was modified thys/Graph_Theory/Funpow.thy (diff)
The file was modified thys/Graph_Theory/Kuratowski.thy (diff)
The file was modified thys/Graph_Theory/Pair_Digraph.thy (diff)
The file was modified thys/Graph_Theory/Shortest_Path.thy (diff)
The file was modified thys/Graph_Theory/Subdivision.thy (diff)
The file was modified thys/Heard_Of/ate/AteProof.thy (diff)
The file was modified thys/Heard_Of/uv/UvProof.thy (diff)
The file was modified thys/Hermite/Hermite.thy (diff)
The file was modified thys/HyperCTL/Deep.thy (diff)
The file was modified thys/HyperCTL/Noninterference.thy (diff)
The file was modified thys/IP_Addresses/IPv6.thy (diff)
The file was modified thys/Incompleteness/Goedel_I.thy (diff)
The file was modified thys/Incompleteness/Pf_Predicates.thy (diff)
The file was modified thys/Incompleteness/Quote.thy (diff)
The file was modified thys/InfPathElimination/RB.thy (diff)
The file was modified thys/InfPathElimination/SymExec.thy (diff)
The file was modified thys/Integration/Integral.thy (diff)
The file was modified thys/Integration/Measure.thy (diff)
The file was modified thys/Integration/MonConv.thy (diff)
The file was modified thys/Iptables_Semantics/Alternative_Semantics.thy (diff)
The file was modified thys/JinjaThreads/Framework/Bisimulation.thy (diff)
The file was modified thys/JinjaThreads/Framework/FWBisimulation.thy (diff)
The file was modified thys/JinjaThreads/Framework/FWInitFinLift.thy (diff)
The file was modified thys/JinjaThreads/Framework/FWLTS.thy (diff)
The file was modified thys/JinjaThreads/Framework/LTS.thy (diff)
The file was modified thys/JinjaThreads/MM/HB_Completion.thy (diff)
The file was modified thys/JinjaThreads/MM/JMM_Framework.thy (diff)
The file was modified thys/JinjaThreads/MM/JMM_Spec.thy (diff)
The file was modified thys/JinjaThreads/MM/JMM_Typesafe.thy (diff)
The file was modified thys/JinjaThreads/MM/JMM_Typesafe2.thy (diff)
The file was modified thys/JinjaThreads/MM/Non_Speculative.thy (diff)
The file was modified thys/JinjaThreads/MM/SC_Completion.thy (diff)
The file was modified thys/JinjaThreads/MM/SC_Legal.thy (diff)
The file was modified thys/Jordan_Hoelder/CompositionSeries.thy (diff)
The file was modified thys/Jordan_Hoelder/JordanHolder.thy (diff)
The file was modified thys/Jordan_Hoelder/MaximalNormalSubgroups.thy (diff)
The file was modified thys/Jordan_Hoelder/SimpleGroups.thy (diff)
The file was modified thys/Jordan_Hoelder/SubgroupsAndNormalSubgroups.thy (diff)
The file was modified thys/Jordan_Normal_Form/DL_Rank.thy (diff)
The file was modified thys/KBPs/SPRViewNonDet.thy (diff)
The file was modified thys/KBPs/SPRViewNonDetIndInit.thy (diff)
The file was modified thys/LOFT/LinuxRouter_OpenFlow_Translation.thy (diff)
The file was modified thys/LTL/LTL.thy (diff)
The file was modified thys/LTL/LTL_Rewrite.thy (diff)
The file was modified thys/LTL_to_DRA/DTS.thy (diff)
The file was modified thys/LTL_to_DRA/Impl/LTL_Rabin_Impl.thy (diff)
The file was modified thys/LTL_to_DRA/LTL_Rabin.thy (diff)
The file was modified thys/LTL_to_DRA/LTL_Rabin_Unfold_Opt.thy (diff)
The file was modified thys/LTL_to_DRA/Logical_Characterization.thy (diff)
The file was modified thys/LTL_to_DRA/Mojmir.thy (diff)
The file was modified thys/LTL_to_DRA/Mojmir_Rabin.thy (diff)
The file was modified thys/LTL_to_DRA/Semi_Mojmir.thy (diff)
The file was modified thys/LTL_to_GBA/LTL_to_GBA.thy (diff)
The file was modified thys/Lam-ml-Normalization/Lam_ml.thy (diff)
The file was modified thys/Landau_Symbols/Landau_Symbols_Definition.thy (diff)
The file was modified thys/Latin_Square/Latin_Square.thy (diff)
The file was modified thys/Launchbury/ResourcedAdequacy.thy (diff)
The file was modified thys/Launchbury/ValueSimilarity.thy (diff)
The file was modified thys/Lazy-Lists-II/LList2.thy (diff)
The file was modified thys/Liouville_Numbers/Liouville_Numbers.thy (diff)
The file was modified thys/List_Update/BIT.thy (diff)
The file was modified thys/List_Update/Move_to_Front.thy (diff)
The file was modified thys/Locally-Nameless-Sigma/Sigma/ParRed.thy (diff)
The file was modified thys/Locally-Nameless-Sigma/Sigma/Sigma.thy (diff)
The file was modified thys/Locally-Nameless-Sigma/Sigma/TypedSigma.thy (diff)
The file was modified thys/Locally-Nameless-Sigma/preliminary/FMap.thy (diff)
The file was modified thys/Lower_Semicontinuous/Lower_Semicontinuous.thy (diff)
The file was modified thys/Markov_Models/Classifying_Markov_Chain_States.thy (diff)
The file was modified thys/Markov_Models/Discrete_Time_Markov_Chain.thy (diff)
The file was modified thys/Markov_Models/MDP_Reachability_Problem.thy (diff)
The file was modified thys/Markov_Models/Markov_Decision_Process.thy (diff)
The file was modified thys/Markov_Models/Markov_Models_Auxiliary.thy (diff)
The file was modified thys/Markov_Models/ex/Crowds_Protocol.thy (diff)
The file was modified thys/Markov_Models/ex/MDP_RP_Certification.thy (diff)
The file was modified thys/Markov_Models/ex/PCTL.thy (diff)
The file was modified thys/Markov_Models/ex/PGCL.thy (diff)
The file was modified thys/Tarskis_Geometry/Hyperbolic_Tarski.thy (diff)
The file was modified thys/Timed_Automata/Approx_Beta.thy (diff)
The file was modified thys/Timed_Automata/Normalized_Zone_Semantics.thy (diff)
Changeset 8574:8ac8a7f5adce by wenzelm:
tuned whitespace;
The file was modified thys/Echelon_Form/ROOT (diff)