Skip to content
Jenkins
log in
Dashboard
afp-repo
#1312
Changes
Status
Changes
Console Output
View Build Information
Polling Log
Timings
Environment Variables
Mercurial Build Data
Embeddable Build Status
Previous Build
Next Build
Success
Changes
Summary
merged
prefer formal comments;
uniform inner and outer comments: isabelle update_cartouches -c;
prefer formal comments;
prefer formal comments;
Changeset
8728:656846d82369
by
wenzelm
:
merged
Changeset
8727:9bc2a5d00cc2
by
wenzelm
:
prefer formal comments;
The file was modified
thys/AVL-Trees/AVL2.thy
(diff)
The file was modified
thys/Abortable_Linearizable_Modules/Simulations.thy
(diff)
The file was modified
thys/Abstract_Soundness/Infinite_Proof_Soundness.thy
(diff)
The file was modified
thys/Affine_Arithmetic/Affine_Approximation.thy
(diff)
The file was modified
thys/Affine_Arithmetic/Print.thy
(diff)
The file was modified
thys/Algebraic_Numbers/Real_Roots.thy
(diff)
The file was modified
thys/AutoFocus-Stream/AF_Stream_Exec.thy
(diff)
The file was modified
thys/Berlekamp_Zassenhaus/Berlekamp_Hensel.thy
(diff)
The file was modified
thys/Berlekamp_Zassenhaus/Berlekamp_Type_Based.thy
(diff)
The file was modified
thys/Berlekamp_Zassenhaus/Factorize_Int_Poly.thy
(diff)
The file was modified
thys/Berlekamp_Zassenhaus/Hensel_Lifting.thy
(diff)
The file was modified
thys/Berlekamp_Zassenhaus/Mahler_Measure.thy
(diff)
The file was modified
thys/Berlekamp_Zassenhaus/Polynomial_Record_Based.thy
(diff)
The file was modified
thys/Berlekamp_Zassenhaus/Reconstruction.thy
(diff)
The file was modified
thys/Berlekamp_Zassenhaus/Square_Free_Factorization_Int.thy
(diff)
The file was modified
thys/CAVA_LTL_Modelchecker/Nested_DFS/NDFS_SI.thy
(diff)
The file was modified
thys/CISC-Kernel/step/Step_invariants.thy
(diff)
The file was modified
thys/CISC-Kernel/trace/Rushby-with-Control/ISK.thy
(diff)
The file was modified
thys/Case_Labeling/Examples/Monadic_Language.thy
(diff)
The file was modified
thys/Collections/Examples/Autoref/Coll_Test.thy
(diff)
The file was modified
thys/Collections/Examples/Autoref/Nested_DFS.thy
(diff)
The file was modified
thys/Collections/ICF/impl/ArrayHashMap.thy
(diff)
The file was modified
thys/Collections/ICF/impl/HashMap.thy
(diff)
The file was modified
thys/ConcurrentGC/MarkObject.thy
(diff)
The file was modified
thys/ConcurrentGC/Model.thy
(diff)
The file was modified
thys/Consensus_Refined/MRU/Three_Step_MRU.thy
(diff)
The file was modified
thys/Consensus_Refined/MRU_Vote_Opt.thy
(diff)
The file was modified
thys/Consensus_Refined/Observing/Two_Step_Observing.thy
(diff)
The file was modified
thys/Consensus_Refined/Observing_Quorums.thy
(diff)
The file was modified
thys/Consensus_Refined/Observing_Quorums_Opt.thy
(diff)
The file was modified
thys/Consensus_Refined/Refinement.thy
(diff)
The file was modified
thys/Consensus_Refined/Same_Vote.thy
(diff)
The file was modified
thys/Consensus_Refined/Voting.thy
(diff)
The file was modified
thys/Consensus_Refined/Voting_Opt.thy
(diff)
The file was modified
thys/DFS_Framework/Impl/Data/Simple_Impl.thy
(diff)
The file was modified
thys/DFS_Framework/Impl/Structural/Tailrec_Impl.thy
(diff)
The file was modified
thys/DFS_Framework/Invars/DFS_Invars_Basic.thy
(diff)
The file was modified
thys/Dependent_SIFUM_Refinement/CompositionalRefinement.thy
(diff)
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/FocusStreamsCaseStudies/Gateway.thy
(diff)
The file was modified
thys/GPU_Kernel_PL/KPL_wellformedness.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_SCC.thy
(diff)
The file was modified
thys/Gabow_SCC/Gabow_Skeleton.thy
(diff)
The file was modified
thys/Game_Based_Crypto/Elgamal.thy
(diff)
The file was modified
thys/Game_Based_Crypto/Hashed_Elgamal.thy
(diff)
The file was modified
thys/GraphMarkingIBP/DSWMark.thy
(diff)
The file was modified
thys/IP_Addresses/CIDR_Split.thy
(diff)
The file was modified
thys/IP_Addresses/IP_Address_Parser.thy
(diff)
The file was modified
thys/IP_Addresses/IP_Address_toString.thy
(diff)
The file was modified
thys/IP_Addresses/IPv6.thy
(diff)
The file was modified
thys/Imperative_Insertion_Sort/Imperative_Insertion_Sort.thy
(diff)
The file was modified
thys/Incredible_Proof_Machine/Incredible_Correctness.thy
(diff)
The file was modified
thys/Iptables_Semantics/Examples/Fail/Ports_Fail.thy
(diff)
The file was modified
thys/Iptables_Semantics/Examples/Parser_Test/Parser6_Test.thy
(diff)
The file was modified
thys/Iptables_Semantics/Examples/SQRL_Shorewall/SQRL_2015_nospoof.thy
(diff)
The file was modified
thys/Iptables_Semantics/Examples/Synology_Diskstation_DS414/Analyze_Synology_Diskstation.thy
(diff)
The file was modified
thys/Iptables_Semantics/Primitive_Matchers/Code_Interface.thy
(diff)
The file was modified
thys/Iptables_Semantics/Primitive_Matchers/No_Spoof.thy
(diff)
The file was modified
thys/Iptables_Semantics/Primitive_Matchers/Output_Interface_Replace.thy
(diff)
The file was modified
thys/Iptables_Semantics/Primitive_Matchers/Ports_Normalize.thy
(diff)
The file was modified
thys/Iptables_Semantics/Primitive_Matchers/Protocols_Normalize.thy
(diff)
The file was modified
thys/Iptables_Semantics/Primitive_Matchers/Transform.thy
(diff)
The file was modified
thys/Iptables_Semantics/Semantics.thy
(diff)
The file was modified
thys/Iptables_Semantics/Semantics_Goto.thy
(diff)
The file was modified
thys/Iptables_Semantics/Semantics_Stateful.thy
(diff)
The file was modified
thys/Iptables_Semantics/Semantics_Ternary/Fixed_Action.thy
(diff)
The file was modified
thys/Iptables_Semantics/Semantics_Ternary/Primitive_Normalization.thy
(diff)
The file was modified
thys/Iptables_Semantics/Semantics_Ternary/Semantics_Ternary.thy
(diff)
The file was modified
thys/JinjaThreads/MM/JMM_Spec.thy
(diff)
The file was modified
thys/Jordan_Normal_Form/Jordan_Normal_Form_Existence.thy
(diff)
The file was modified
thys/LOFT/LinuxRouter_OpenFlow_Translation.thy
(diff)
The file was modified
thys/LOFT/OpenFlow_Documentation.thy
(diff)
The file was modified
thys/LTL_to_DRA/Impl/LTL_Rabin_Impl.thy
(diff)
The file was modified
thys/Latin_Square/Latin_Square.thy
(diff)
The file was modified
thys/List-Infinite/ListInf/List2.thy
(diff)
The file was modified
thys/List-Infinite/ListInf/ListInf.thy
(diff)
The file was modified
thys/List-Infinite/ListInf/ListInf_Prefix.thy
(diff)
The file was modified
thys/List_Update/TS.thy
(diff)
The file was modified
thys/Modal_Logics_for_NTS/Weak_Transition_System.thy
(diff)
The file was modified
thys/Network_Security_Policy_Verification/Examples/Distributed_WebApp.thy
(diff)
The file was modified
thys/Network_Security_Policy_Verification/Examples/Imaginary_Factory_Network.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/Security_Invariants/METASINVAR_SystemBoundary.thy
(diff)
The file was modified
thys/Ordinary_Differential_Equations/Ex/Examples_One_Step_Method.thy
(diff)
The file was modified
thys/Ordinary_Differential_Equations/Ex/Lorenz/Lorenz_Approximation.thy
(diff)
The file was modified
thys/Ordinary_Differential_Equations/Numerics/Example_Utilities.thy
(diff)
The file was modified
thys/Ordinary_Differential_Equations/Numerics/Refine_Reachability_Analysis.thy
(diff)
The file was modified
thys/PCF/PCF.thy
(diff)
The file was modified
thys/PLM/TAO_2_Semantics.thy
(diff)
The file was modified
thys/Perron_Frobenius/Spectral_Radius_Theory_2.thy
(diff)
The file was modified
thys/Polynomial_Factorization/Prime_Factorization.thy
(diff)
The file was modified
thys/Promela/Promela.thy
(diff)
The file was modified
thys/Promela/PromelaDatastructures.thy
(diff)
The file was modified
thys/Propositional_Proof_Systems/Formulas.thy
(diff)
The file was modified
thys/ROBDD/Level_Collapse.thy
(diff)
The file was modified
thys/Recursion-Theory-I/PRecUnGr.thy
(diff)
The file was modified
thys/Refine_Imperative_HOL/Examples/Sepref_WGraph.thy
(diff)
The file was modified
thys/Refine_Imperative_HOL/Examples/Snippets/Sepref_Snip_Datatype.thy
(diff)
The file was modified
thys/Refine_Imperative_HOL/IICF/Impl/Heaps/IICF_Impl_Heapmap.thy
(diff)
The file was modified
thys/Refine_Imperative_HOL/IICF/Impl/IICF_Array_Matrix.thy
(diff)
The file was modified
thys/Refine_Imperative_HOL/Userguides/Sepref_Guide_Quickstart.thy
(diff)
The file was modified
thys/Refine_Monadic/Refine_Misc.thy
(diff)
The file was modified
thys/Routing/Linux_Router.thy
(diff)
The file was modified
thys/Separation_Logic_Imperative_HOL/Examples/Array_Blit.thy
(diff)
The file was modified
thys/Separation_Logic_Imperative_HOL/Examples/Circ_List.thy
(diff)
The file was modified
thys/Stirling_Formula/Ln_Gamma_Asymptotics.thy
(diff)
The file was modified
thys/UPF/Monads.thy
(diff)
The file was modified
thys/Vickrey_Clarke_Groves/Partitions.thy
(diff)
Changeset
8726:5e5c48e5c72f
by
wenzelm
:
uniform inner and outer comments: isabelle update_cartouches -c;
The file was modified
thys/Key_Agreement_Strong_Adversaries/AuthenticationI.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/AuthenticationN.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/Channels.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/IK.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/Implem.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/Implem_asymmetric.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/Implem_lemmas.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/Implem_symmetric.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/Infra.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/Message_derivation.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/Messages.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/Payloads.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/Refinement.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/Runs.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/Secrecy.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/dhlvl1.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/dhlvl2.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/dhlvl3.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/dhlvl3_asymmetric.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/dhlvl3_symmetric.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/pfslvl1.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/pfslvl2.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/pfslvl3.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/pfslvl3_asymmetric.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/pfslvl3_symmetric.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/sklvl1.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/sklvl2.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/sklvl3.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/sklvl3_asymmetric.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/sklvl3_symmetric.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Auth_simple/m1_auth.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Auth_simple/m2_auth_chan.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Auth_simple/m2_confid_chan.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Auth_simple/m3_enc.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/m1_ds.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Key_establish/m1_kerberos.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Key_establish/m1_keydist.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Key_establish/m1_keydist_iirn.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Key_establish/m1_keydist_inrn.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Key_establish/m1_nssk.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Key_establish/m2_ds.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/Security_Protocol_Refinement/Key_establish/m3_ds.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Key_establish/m3_ds_par.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Key_establish/m3_kerberos4.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Key_establish/m3_kerberos5.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Key_establish/m3_kerberos_par.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Key_establish/m3_nssk.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Key_establish/m3_nssk_par.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Refinement/Agents.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Refinement/Atoms.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Refinement/Channels.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Refinement/Infra.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Refinement/Keys.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Refinement/Message.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Refinement/Refinement.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Refinement/Runs.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Refinement/a0i_agree.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Refinement/a0n_agree.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Refinement/s0g_secrecy.thy
(diff)
Changeset
8725:4c384402fbdb
by
wenzelm
:
prefer formal comments;
The file was modified
thys/Key_Agreement_Strong_Adversaries/AuthenticationI.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/AuthenticationN.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/IK.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/Implem_lemmas.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/Message_derivation.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/Payloads.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/Refinement.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/Secrecy.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/dhlvl1.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/dhlvl2.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/dhlvl3.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/pfslvl1.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/pfslvl2.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/pfslvl3.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/sklvl1.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/sklvl2.thy
(diff)
The file was modified
thys/Key_Agreement_Strong_Adversaries/sklvl3.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Auth_simple/m1_auth.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Auth_simple/m2_auth_chan.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Auth_simple/m2_confid_chan.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Auth_simple/m3_enc.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/m1_ds.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Key_establish/m1_kerberos.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Key_establish/m1_keydist.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Key_establish/m1_keydist_iirn.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Key_establish/m1_keydist_inrn.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Key_establish/m1_nssk.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Key_establish/m2_ds.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/Security_Protocol_Refinement/Key_establish/m3_ds.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Key_establish/m3_ds_par.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Key_establish/m3_kerberos4.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Key_establish/m3_kerberos5.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Key_establish/m3_kerberos_par.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Key_establish/m3_nssk.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Key_establish/m3_nssk_par.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Refinement/Agents.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Refinement/Refinement.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Refinement/a0i_agree.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Refinement/a0n_agree.thy
(diff)
The file was modified
thys/Security_Protocol_Refinement/Refinement/s0g_secrecy.thy
(diff)
Changeset
8724:d2977e824cd2
by
wenzelm
:
prefer formal comments;
The file was modified
thys/Isabelle_Meta_Model/Init.thy
(diff)
The file was modified
thys/Isabelle_Meta_Model/meta_isabelle/Meta_Isabelle.thy
(diff)
The file was modified
thys/Isabelle_Meta_Model/meta_isabelle/Meta_SML.thy
(diff)
The file was modified
thys/Isabelle_Meta_Model/meta_isabelle/Parser_init.thy
(diff)
The file was modified
thys/Isabelle_Meta_Model/meta_isabelle/Printer_Isabelle.thy
(diff)
The file was modified
thys/Isabelle_Meta_Model/meta_isabelle/Printer_Pure.thy
(diff)
The file was modified
thys/Isabelle_Meta_Model/meta_isabelle/Printer_SML.thy
(diff)
The file was modified
thys/Isabelle_Meta_Model/meta_isabelle/Printer_init.thy
(diff)
The file was modified
thys/Isabelle_Meta_Model/toy_example/embedding/Core.thy
(diff)
The file was modified
thys/Isabelle_Meta_Model/toy_example/embedding/Init_rbt.thy
(diff)
The file was modified
thys/Isabelle_Meta_Model/toy_example/embedding/Printer.thy
(diff)
The file was modified
thys/Isabelle_Meta_Model/toy_example/embedding/core/Core_init.thy
(diff)
The file was modified
thys/Isabelle_Meta_Model/toy_example/embedding/core/Floor1_access.thy
(diff)
The file was modified
thys/Isabelle_Meta_Model/toy_example/embedding/meta_toy/Meta_META.thy
(diff)
The file was modified
thys/Isabelle_Meta_Model/toy_example/embedding/meta_toy/Meta_Toy.thy
(diff)
The file was modified
thys/Isabelle_Meta_Model/toy_example/embedding/meta_toy/Meta_Toy_extended.thy
(diff)
The file was modified
thys/Isabelle_Meta_Model/toy_example/embedding/meta_toy/Parser_META.thy
(diff)
The file was modified
thys/Isabelle_Meta_Model/toy_example/embedding/meta_toy/Printer_META.thy
(diff)
The file was modified
thys/Isabelle_Meta_Model/toy_example/embedding/meta_toy/Printer_Toy.thy
(diff)
The file was modified
thys/Isabelle_Meta_Model/toy_example/embedding/meta_toy/Printer_Toy_extended.thy
(diff)