Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. simplified;
  2. merged
  3. non-executable files;
  4. clarified formal comments;
  5. prefer formal comments; avoid outer verbatim token: Thy_Output.token / Antiquote.parse fails due to partitioning in operator ranges;
  6. clarified formal comment, based on version before 3ccb204d9c5f and educated guessing;
  7. prefer formal comments;
  8. \usepackage[normalem]{ulem} is already provided by isabelle.sty (Isabelle/efc9ec539224);
  9. removed old/unused clones of Isabelle distribution files;
Changeset 8755:f787608b0ab7 by wenzelm:
simplified;
The file was modified thys/CAVA_LTL_Modelchecker/Nested_DFS/NDFS_SI.thy (diff)
Changeset 8754:94d7756d8823 by wenzelm:
merged
Changeset 8753:05037570348f by wenzelm:
non-executable files;
The file was modified thys/Bernoulli/document/root.bib (diff)
The file was modified thys/Bernoulli/document/root.tex (diff)
The file was modified thys/Bertrands_Postulate/document/root.bib (diff)
The file was modified thys/Bertrands_Postulate/document/root.tex (diff)
The file was modified thys/Cayley_Hamilton/document/root.bib (diff)
The file was modified thys/Cayley_Hamilton/document/root.tex (diff)
The file was modified thys/ComponentDependencies/document/root.bib (diff)
The file was modified thys/Count_Complex_Roots/ROOT (diff)
The file was modified thys/Count_Complex_Roots/document/root.bib (diff)
The file was modified thys/Count_Complex_Roots/document/root.tex (diff)
The file was modified thys/Deep_Learning/DL_Missing_Finite_Set.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/Tensor.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/Deep_Learning/Tensor_Scalar_Mult.thy (diff)
The file was modified thys/Deep_Learning/Tensor_Subtensor.thy (diff)
The file was modified thys/Deep_Learning/Tensor_Unit_Vec.thy (diff)
The file was modified thys/Deep_Learning/document/root.bib (diff)
The file was modified thys/Deep_Learning/document/root.tex (diff)
The file was modified thys/DynamicArchitectures/Dynamic_Architecture_Calculus.thy (diff)
The file was modified thys/DynamicArchitectures/document/root.bib (diff)
The file was modified thys/DynamicArchitectures/document/root.tex (diff)
The file was modified thys/Ergodic_Theory/ROOT (diff)
The file was modified thys/Ergodic_Theory/document/root.tex (diff)
The file was modified thys/FOL_Harrison/document/root.tex (diff)
The file was modified thys/Finite_Automata_HF/document/root.tex (diff)
The file was modified thys/Floyd_Warshall/document/root.bib (diff)
The file was modified thys/Gauss_Jordan/document/root.bib (diff)
The file was modified thys/IMAP-CRDT/IMAP-def.thy (diff)
The file was modified thys/IMAP-CRDT/IMAP-proof-commute.thy (diff)
The file was modified thys/IMAP-CRDT/IMAP-proof-helpers.thy (diff)
The file was modified thys/IMAP-CRDT/IMAP-proof-independent.thy (diff)
The file was modified thys/IMAP-CRDT/IMAP-proof.thy (diff)
The file was modified thys/IMAP-CRDT/document/root.bib (diff)
The file was modified thys/IMAP-CRDT/document/root.tex (diff)
The file was modified thys/Jordan_Normal_Form/DL_Missing_List.thy (diff)
The file was modified thys/Jordan_Normal_Form/DL_Missing_Sublist.thy (diff)
The file was modified thys/Jordan_Normal_Form/DL_Rank_Submatrix.thy (diff)
The file was modified thys/LTL_to_DRA/Rabin.thy (diff)
The file was modified thys/Lp/Lp.thy (diff)
The file was modified thys/Lp/ROOT (diff)
The file was modified thys/Lp/document/root.tex (diff)
The file was modified thys/No_FTL_observers/Axioms.thy (diff)
The file was modified thys/No_FTL_observers/ROOT (diff)
The file was modified thys/No_FTL_observers/SomeFunc.thy (diff)
The file was modified thys/No_FTL_observers/SpaceTime.thy (diff)
The file was modified thys/No_FTL_observers/SpecRel.thy (diff)
The file was modified thys/No_FTL_observers/document/root.tex (diff)
The file was modified thys/Noninterference_Inductive_Unwinding/document/root.bib (diff)
The file was modified thys/Noninterference_Inductive_Unwinding/document/root.tex (diff)
The file was modified thys/Noninterference_Sequential_Composition/Counterexamples.thy (diff)
The file was modified thys/Noninterference_Sequential_Composition/SequentialComposition.thy (diff)
The file was modified thys/Noninterference_Sequential_Composition/document/root.bib (diff)
The file was modified thys/Noninterference_Sequential_Composition/document/root.tex (diff)
The file was modified thys/Optics/document/figures/Lens.pdf (diff)
The file was modified thys/Optics/document/figures/parallel-by-merge.pdf (diff)
The file was modified thys/Orbit_Stabiliser/ROOT (diff)
The file was modified thys/Orbit_Stabiliser/document/root.bib (diff)
The file was modified thys/Orbit_Stabiliser/document/root.tex (diff)
The file was modified thys/Password_Authentication_Protocol/Protocol.thy (diff)
The file was modified thys/Password_Authentication_Protocol/document/root.bib (diff)
The file was modified thys/Password_Authentication_Protocol/document/root.tex (diff)
The file was modified thys/Pop_Refinement/document/root.bib (diff)
The file was modified thys/Pop_Refinement/document/root.tex (diff)
The file was modified thys/PropResPI/document/root.tex (diff)
The file was modified thys/Ptolemys_Theorem/ROOT (diff)
The file was modified thys/Ptolemys_Theorem/document/root.bib (diff)
The file was modified thys/Ptolemys_Theorem/document/root.tex (diff)
The file was modified thys/Stirling_Formula/document/root.tex (diff)
The file was modified thys/Sturm_Tarski/document/root.bib (diff)
The file was modified thys/Sturm_Tarski/document/root.tex (diff)
The file was modified thys/SuperCalc/document/root.bib (diff)
The file was modified thys/SuperCalc/document/root.tex (diff)
The file was modified thys/SuperCalc/well_founded_continued.thy (diff)
The file was modified thys/Timed_Automata/document/root.bib (diff)
The file was modified thys/VectorSpace/ROOT (diff)
The file was modified thys/VectorSpace/document/root.tex (diff)
The file was modified thys/Winding_Number_Eval/ROOT (diff)
The file was modified thys/Winding_Number_Eval/document/root.bib (diff)
The file was modified thys/Winding_Number_Eval/document/root.tex (diff)
The file was modified web/entries/Depth-First-Search.html (diff)
Changeset 8752:e48acbc6a46f by wenzelm:
clarified formal comments;
The file was modified thys/Dependent_SIFUM_Refinement/Examples/Eg1Eg2RefinementSimple.thy (diff)
The file was modified thys/Dependent_SIFUM_Refinement/Examples/EgHighBranchRevC.thy (diff)
The file was modified thys/SPARCv8/SparcModel_MMU/Sparc_Execution.thy (diff)
Changeset 8751:5fe2cb04065a by wenzelm:
prefer formal comments;<br>avoid outer verbatim token: Thy_Output.token / Antiquote.parse fails due to partitioning in operator ranges;
The file was modified thys/Network_Security_Policy_Verification/Examples/Imaginary_Factory_Network.thy (diff)
Changeset 8750:3704709fc0b6 by wenzelm:
clarified formal comment, based on version before 3ccb204d9c5f and educated guessing;
The file was modified thys/SPARCv8/SparcModel_MMU/Sparc_Instruction.thy (diff)
Changeset 8749:e1fed5097c39 by wenzelm:
prefer formal comments;
The file was modified thys/Abs_Int_ITP2012/Abs_Int2_ivl.thy (diff)
The file was modified thys/Abs_Int_ITP2012/Abs_Int3.thy (diff)
The file was modified thys/Allen_Calculus/nest.thy (diff)
The file was modified thys/Berlekamp_Zassenhaus/Berlekamp_Zassenhaus.thy (diff)
The file was modified thys/CAVA_Automata/Digraph_Impl.thy (diff)
The file was modified thys/Collections/Examples/ICF/Exploration_DFS.thy (diff)
The file was modified thys/Complx/SmallStep.thy (diff)
The file was modified thys/CoreC++/Equivalence.thy (diff)
The file was modified thys/CoreC++/Progress.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/Impl/Structural/Rec_Impl.thy (diff)
The file was modified thys/DFS_Framework/Impl/Structural/Tailrec_Impl.thy (diff)
The file was modified thys/Differential_Dynamic_Logic/Proof_Checker.thy (diff)
The file was modified thys/Diophantine_Eqns_Lin_Hom/Algorithm.thy (diff)
The file was modified thys/Featherweight_OCL/examples/Employee_Model/Analysis/Analysis_UML.thy (diff)
The file was modified thys/Featherweight_OCL/examples/Employee_Model/Design/Design_UML.thy (diff)
The file was modified thys/GPU_Kernel_PL/KPL_execution_thread.thy (diff)
The file was modified thys/Gabow_SCC/Gabow_GBG.thy (diff)
The file was modified thys/Gabow_SCC/Gabow_SCC.thy (diff)
The file was modified thys/Green/Green.thy (diff)
The file was modified thys/HotelKeyCards/Trace.thy (diff)
The file was modified thys/Iptables_Semantics/Datatype_Selectors.thy (diff)
The file was modified thys/Iptables_Semantics/Primitive_Matchers/Ipassmt.thy (diff)
The file was modified thys/Isabelle_Meta_Model/toy_example/embedding/core/Floor1_infra.thy (diff)
The file was modified thys/Isabelle_Meta_Model/toy_example/embedding/meta_toy/Meta_Toy.thy (diff)
The file was modified thys/Jinja/J/Progress.thy (diff)
The file was modified thys/LOFT/Examples/OF_conv_test/OF_conv_test.thy (diff)
The file was modified thys/LTL_to_GBA/LTL_to_GBA_impl.thy (diff)
The file was modified thys/List_Update/List_Factoring.thy (diff)
The file was modified thys/Network_Security_Policy_Verification/Examples/Tainting/MeasrDroid.thy (diff)
The file was modified thys/Network_Security_Policy_Verification/SINVAR_Examples.thy (diff)
The file was modified thys/Network_Security_Policy_Verification/TopoS_Stateful_Policy_Algorithm.thy (diff)
The file was modified thys/Ordinary_Differential_Equations/Numerics/Refine_Reachability_Analysis.thy (diff)
The file was modified thys/Prpu_Maxflow/Fifo_Push_Relabel_Impl.thy (diff)
The file was modified thys/Prpu_Maxflow/Relabel_To_Front_Impl.thy (diff)
The file was modified thys/Refine_Imperative_HOL/Examples/Sepref_Minitests.thy (diff)
The file was modified thys/Refine_Imperative_HOL/Userguides/Sepref_Guide_Quickstart.thy (diff)
The file was modified thys/Refine_Monadic/Generic/RefineG_Recursion.thy (diff)
The file was modified thys/Regex_Equivalence/Benchmark.thy (diff)
The file was modified thys/Root_Balanced_Tree/Root_Balanced_Tree_Tab.thy (diff)
The file was modified thys/SPARCv8/SparcModel_MMU/Sparc_Init_State.thy (diff)
The file was modified thys/SPARCv8/SparcModel_MMU/Sparc_Instruction.thy (diff)
The file was modified thys/SPARCv8/SparcModel_MMU/Sparc_State.thy (diff)
The file was modified thys/SPARCv8/SparcModel_MMU/Sparc_Types.thy (diff)
The file was modified thys/Security_Protocol_Refinement/Auth_simple/m3_sig.thy (diff)
The file was modified thys/Security_Protocol_Refinement/Key_establish/m2_kerberos.thy (diff)
The file was modified thys/Security_Protocol_Refinement/Key_establish/m2_nssk.thy (diff)
The file was modified thys/Simpl/UserGuide.thy (diff)
The file was modified thys/Simple_Firewall/Service_Matrix.thy (diff)
The file was modified thys/Taylor_Models/Taylor_Models.thy (diff)
The file was modified thys/Tree-Automata/Ta_impl.thy (diff)
Changeset 8748:440d36307bef by wenzelm:
\usepackage[normalem]{ulem} is already provided by isabelle.sty (Isabelle/efc9ec539224);
The file was modified thys/Shivers-CFA/document/root.tex (diff)
Changeset 8747:1f38f7a75cb9 by wenzelm:
removed old/unused clones of Isabelle distribution files;
The file was removedthys/Optics/document/comment.sty
The file was removedthys/Optics/document/isabelle.sty
The file was removedthys/Optics/document/isabellesym.sty
The file was removedthys/Optics/document/isabelletags.sty
The file was removedthys/Optics/document/pdfsetup.sty
The file was removedthys/Optics/document/railsetup.sty