Skip to content
Jenkins
log in
Dashboard
Benedikt Seidl <benedikt.seidl@tum.de>
My Views
All
isabelle-repo
#1464
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
more symbols;
Changeset
67614:560fbd6bc047
by
wenzelm
:
merged
Changeset
67613:ce654b0e6d69
by
wenzelm
:
more symbols;
The file was modified
src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy
(diff)
The file was modified
src/Doc/Prog_Prove/Isar.thy
(diff)
The file was modified
src/Doc/Prog_Prove/Logic.thy
(diff)
The file was modified
src/Doc/Prog_Prove/Types_and_funs.thy
(diff)
The file was modified
src/Doc/Sugar/Sugar.thy
(diff)
The file was modified
src/Doc/Tutorial/CTL/CTL.thy
(diff)
The file was modified
src/Doc/Tutorial/CTL/PDL.thy
(diff)
The file was modified
src/Doc/Tutorial/Ifexpr/Ifexpr.thy
(diff)
The file was modified
src/Doc/Tutorial/Inductive/Mutual.thy
(diff)
The file was modified
src/Doc/Tutorial/Inductive/Star.thy
(diff)
The file was modified
src/Doc/Tutorial/Misc/Plus.thy
(diff)
The file was modified
src/Doc/Tutorial/Misc/Tree2.thy
(diff)
The file was modified
src/Doc/Tutorial/Misc/prime_def.thy
(diff)
The file was modified
src/Doc/Tutorial/Protocol/Event.thy
(diff)
The file was modified
src/Doc/Tutorial/Protocol/Message.thy
(diff)
The file was modified
src/Doc/Tutorial/Protocol/Public.thy
(diff)
The file was modified
src/Doc/Tutorial/Rules/TPrimes.thy
(diff)
The file was modified
src/Doc/Tutorial/Sets/Examples.thy
(diff)
The file was modified
src/HOL/Algebra/AbelCoset.thy
(diff)
The file was modified
src/HOL/Algebra/FiniteProduct.thy
(diff)
The file was modified
src/HOL/Algebra/Group.thy
(diff)
The file was modified
src/HOL/Algebra/Order.thy
(diff)
The file was modified
src/HOL/Algebra/Ring.thy
(diff)
The file was modified
src/HOL/Algebra/RingHom.thy
(diff)
The file was modified
src/HOL/Algebra/Sylow.thy
(diff)
The file was modified
src/HOL/Algebra/UnivPoly.thy
(diff)
The file was modified
src/HOL/Analysis/Arcwise_Connected.thy
(diff)
The file was modified
src/HOL/Analysis/Cauchy_Integral_Theorem.thy
(diff)
The file was modified
src/HOL/Analysis/Continuous_Extension.thy
(diff)
The file was modified
src/HOL/Analysis/Convex_Euclidean_Space.thy
(diff)
The file was modified
src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
(diff)
The file was modified
src/HOL/Analysis/Extended_Real_Limits.thy
(diff)
The file was modified
src/HOL/Analysis/Polytope.thy
(diff)
The file was modified
src/HOL/Analysis/Starlike.thy
(diff)
The file was modified
src/HOL/Analysis/Topology_Euclidean_Space.thy
(diff)
The file was modified
src/HOL/Auth/CertifiedEmail.thy
(diff)
The file was modified
src/HOL/Auth/Event.thy
(diff)
The file was modified
src/HOL/Auth/Guard/Analz.thy
(diff)
The file was modified
src/HOL/Auth/Guard/Extensions.thy
(diff)
The file was modified
src/HOL/Auth/Guard/Guard.thy
(diff)
The file was modified
src/HOL/Auth/Guard/GuardK.thy
(diff)
The file was modified
src/HOL/Auth/Guard/Guard_NS_Public.thy
(diff)
The file was modified
src/HOL/Auth/Guard/Guard_OtwayRees.thy
(diff)
The file was modified
src/HOL/Auth/Guard/Guard_Public.thy
(diff)
The file was modified
src/HOL/Auth/Guard/Guard_Shared.thy
(diff)
The file was modified
src/HOL/Auth/Guard/Guard_Yahalom.thy
(diff)
The file was modified
src/HOL/Auth/Guard/List_Msg.thy
(diff)
The file was modified
src/HOL/Auth/Guard/P1.thy
(diff)
The file was modified
src/HOL/Auth/Guard/P2.thy
(diff)
The file was modified
src/HOL/Auth/Guard/Proto.thy
(diff)
The file was modified
src/HOL/Auth/KerberosIV.thy
(diff)
The file was modified
src/HOL/Auth/KerberosIV_Gets.thy
(diff)
The file was modified
src/HOL/Auth/KerberosV.thy
(diff)
The file was modified
src/HOL/Auth/Kerberos_BAN.thy
(diff)
The file was modified
src/HOL/Auth/Kerberos_BAN_Gets.thy
(diff)
The file was modified
src/HOL/Auth/Message.thy
(diff)
The file was modified
src/HOL/Auth/NS_Shared.thy
(diff)
The file was modified
src/HOL/Auth/OtwayRees.thy
(diff)
The file was modified
src/HOL/Auth/OtwayReesBella.thy
(diff)
The file was modified
src/HOL/Auth/OtwayRees_AN.thy
(diff)
The file was modified
src/HOL/Auth/OtwayRees_Bad.thy
(diff)
The file was modified
src/HOL/Auth/Public.thy
(diff)
The file was modified
src/HOL/Auth/Recur.thy
(diff)
The file was modified
src/HOL/Auth/Shared.thy
(diff)
The file was modified
src/HOL/Auth/Smartcard/Smartcard.thy
(diff)
The file was modified
src/HOL/Auth/TLS.thy
(diff)
The file was modified
src/HOL/Auth/WooLam.thy
(diff)
The file was modified
src/HOL/Auth/Yahalom.thy
(diff)
The file was modified
src/HOL/Auth/Yahalom2.thy
(diff)
The file was modified
src/HOL/Auth/Yahalom_Bad.thy
(diff)
The file was modified
src/HOL/BNF_Cardinal_Arithmetic.thy
(diff)
The file was modified
src/HOL/BNF_Cardinal_Order_Relation.thy
(diff)
The file was modified
src/HOL/BNF_Composition.thy
(diff)
The file was modified
src/HOL/BNF_Def.thy
(diff)
The file was modified
src/HOL/BNF_Greatest_Fixpoint.thy
(diff)
The file was modified
src/HOL/BNF_Wellorder_Constructions.thy
(diff)
The file was modified
src/HOL/BNF_Wellorder_Embedding.thy
(diff)
The file was modified
src/HOL/Bali/AxCompl.thy
(diff)
The file was modified
src/HOL/Bali/AxSem.thy
(diff)
The file was modified
src/HOL/Bali/AxSound.thy
(diff)
The file was modified
src/HOL/Bali/Basis.thy
(diff)
The file was modified
src/HOL/Bali/Decl.thy
(diff)
The file was modified
src/HOL/Bali/DeclConcepts.thy
(diff)
The file was modified
src/HOL/Bali/Example.thy
(diff)
The file was modified
src/HOL/Bali/Table.thy
(diff)
The file was modified
src/HOL/Bali/TypeRel.thy
(diff)
The file was modified
src/HOL/Bali/WellForm.thy
(diff)
The file was modified
src/HOL/Cardinals/Cardinal_Order_Relation.thy
(diff)
The file was modified
src/HOL/Cardinals/Wellorder_Constructions.thy
(diff)
The file was modified
src/HOL/Complete_Lattices.thy
(diff)
The file was modified
src/HOL/Computational_Algebra/Primes.thy
(diff)
The file was modified
src/HOL/Conditionally_Complete_Lattices.thy
(diff)
The file was modified
src/HOL/Data_Structures/AA_Map.thy
(diff)
The file was modified
src/HOL/Data_Structures/AA_Set.thy
(diff)
The file was modified
src/HOL/Data_Structures/Brother12_Set.thy
(diff)
The file was modified
src/HOL/Decision_Procs/MIR.thy
(diff)
The file was modified
src/HOL/Decision_Procs/approximation.ML
(diff)
The file was modified
src/HOL/Enum.thy
(diff)
The file was modified
src/HOL/Filter.thy
(diff)
The file was modified
src/HOL/Fun_Def.thy
(diff)
The file was modified
src/HOL/HOLCF/FOCUS/Buffer.thy
(diff)
The file was modified
src/HOL/HOLCF/FOCUS/Buffer_adm.thy
(diff)
The file was modified
src/HOL/HOLCF/FOCUS/FOCUS.thy
(diff)
The file was modified
src/HOL/HOLCF/FOCUS/Fstream.thy
(diff)
The file was modified
src/HOL/HOLCF/FOCUS/Stream_adm.thy
(diff)
The file was modified
src/HOL/HOLCF/IMP/Denotational.thy
(diff)
The file was modified
src/HOL/HOLCF/IOA/ABP/Lemmas.thy
(diff)
The file was modified
src/HOL/HOLCF/IOA/CompoExecs.thy
(diff)
The file was modified
src/HOL/HOLCF/IOA/CompoScheds.thy
(diff)
The file was modified
src/HOL/HOLCF/IOA/CompoTraces.thy
(diff)
The file was modified
src/HOL/HOLCF/IOA/NTP/Abschannel.thy
(diff)
The file was modified
src/HOL/HOLCF/IOA/NTP/Correctness.thy
(diff)
The file was modified
src/HOL/HOLCF/IOA/NTP/Impl.thy
(diff)
The file was modified
src/HOL/HOLCF/IOA/NTP/Lemmas.thy
(diff)
The file was modified
src/HOL/HOLCF/IOA/NTP/Multiset.thy
(diff)
The file was modified
src/HOL/HOLCF/IOA/NTP/Packet.thy
(diff)
The file was modified
src/HOL/HOLCF/IOA/NTP/Receiver.thy
(diff)
The file was modified
src/HOL/HOLCF/IOA/NTP/Sender.thy
(diff)
The file was modified
src/HOL/HOLCF/IOA/NTP/Spec.thy
(diff)
The file was modified
src/HOL/HOLCF/IOA/RefCorrectness.thy
(diff)
The file was modified
src/HOL/HOLCF/IOA/SimCorrectness.thy
(diff)
The file was modified
src/HOL/HOLCF/IOA/Simulations.thy
(diff)
The file was modified
src/HOL/HOLCF/IOA/Storage/Action.thy
(diff)
The file was modified
src/HOL/HOLCF/IOA/Storage/Correctness.thy
(diff)
The file was modified
src/HOL/HOLCF/IOA/Storage/Impl.thy
(diff)
The file was modified
src/HOL/HOLCF/IOA/Storage/Spec.thy
(diff)
The file was modified
src/HOL/HOLCF/Library/Stream.thy
(diff)
The file was modified
src/HOL/HOLCF/Tools/Domain/domain_induction.ML
(diff)
The file was modified
src/HOL/HOLCF/ex/Loop.thy
(diff)
The file was modified
src/HOL/Hilbert_Choice.thy
(diff)
The file was modified
src/HOL/Hoare/Arith2.thy
(diff)
The file was modified
src/HOL/Hoare/Examples.thy
(diff)
The file was modified
src/HOL/Hoare/Heap.thy
(diff)
The file was modified
src/HOL/Hoare/Hoare_Logic.thy
(diff)
The file was modified
src/HOL/Hoare/Hoare_Logic_Abort.thy
(diff)
The file was modified
src/HOL/Hoare/Pointer_Examples.thy
(diff)
The file was modified
src/HOL/Hoare/Pointers0.thy
(diff)
The file was modified
src/HOL/Hoare_Parallel/RG_Tran.thy
(diff)
The file was modified
src/HOL/IMP/ACom.thy
(diff)
The file was modified
src/HOL/IMP/Abs_Int0.thy
(diff)
The file was modified
src/HOL/IMP/Abs_Int1.thy
(diff)
The file was modified
src/HOL/IMP/Abs_Int2.thy
(diff)
The file was modified
src/HOL/IMP/Abs_Int2_ivl.thy
(diff)
The file was modified
src/HOL/IMP/Abs_Int3.thy
(diff)
The file was modified
src/HOL/IMP/Abs_State.thy
(diff)
The file was modified
src/HOL/IMP/Collecting.thy
(diff)
The file was modified
src/HOL/IMP/Collecting1.thy
(diff)
The file was modified
src/HOL/IMP/Complete_Lattice.thy
(diff)
The file was modified
src/HOL/IMP/Def_Init_Small.thy
(diff)
The file was modified
src/HOL/IMP/Denotational.thy
(diff)
The file was modified
src/HOL/IMP/Fold.thy
(diff)
The file was modified
src/HOL/IMP/Live.thy
(diff)
The file was modified
src/HOL/IMP/Small_Step.thy
(diff)
The file was modified
src/HOL/IMP/VCG_Total_EX.thy
(diff)
The file was modified
src/HOL/IMP/VCG_Total_EX2.thy
(diff)
The file was modified
src/HOL/IMPP/Com.thy
(diff)
The file was modified
src/HOL/IMPP/Hoare.thy
(diff)
The file was modified
src/HOL/IMPP/Misc.thy
(diff)
The file was modified
src/HOL/IMPP/Natural.thy
(diff)
The file was modified
src/HOL/IOA/Asig.thy
(diff)
The file was modified
src/HOL/IOA/IOA.thy
(diff)
The file was modified
src/HOL/IOA/Solve.thy
(diff)
The file was modified
src/HOL/Induct/SList.thy
(diff)
The file was modified
src/HOL/Induct/Sexp.thy
(diff)
The file was modified
src/HOL/Isar_Examples/Hoare.thy
(diff)
The file was modified
src/HOL/Lattices_Big.thy
(diff)
The file was modified
src/HOL/Library/BNF_Corec.thy
(diff)
The file was modified
src/HOL/Library/Countable_Set.thy
(diff)
The file was modified
src/HOL/Library/IArray.thy
(diff)
The file was modified
src/HOL/Library/Lub_Glb.thy
(diff)
The file was modified
src/HOL/Library/Old_Datatype.thy
(diff)
The file was modified
src/HOL/Library/Stream.thy
(diff)
The file was modified
src/HOL/Library/Sublist.thy
(diff)
The file was modified
src/HOL/Library/While_Combinator.thy
(diff)
The file was modified
src/HOL/List.thy
(diff)
The file was modified
src/HOL/Matrix_LP/ComputeFloat.thy
(diff)
The file was modified
src/HOL/Matrix_LP/Matrix.thy
(diff)
The file was modified
src/HOL/Matrix_LP/SparseMatrix.thy
(diff)
The file was modified
src/HOL/Metis_Examples/Big_O.thy
(diff)
The file was modified
src/HOL/Metis_Examples/Clausification.thy
(diff)
The file was modified
src/HOL/Metis_Examples/Message.thy
(diff)
The file was modified
src/HOL/Metis_Examples/Sets.thy
(diff)
The file was modified
src/HOL/Metis_Examples/Tarski.thy
(diff)
The file was modified
src/HOL/MicroJava/BV/BVExample.thy
(diff)
The file was modified
src/HOL/MicroJava/BV/JType.thy
(diff)
The file was modified
src/HOL/MicroJava/BV/Typing_Framework_JVM.thy
(diff)
The file was modified
src/HOL/MicroJava/Comp/CorrComp.thy
(diff)
The file was modified
src/HOL/MicroJava/Comp/LemmasComp.thy
(diff)
The file was modified
src/HOL/MicroJava/DFA/Err.thy
(diff)
The file was modified
src/HOL/MicroJava/DFA/Kildall.thy
(diff)
The file was modified
src/HOL/MicroJava/DFA/Listn.thy
(diff)
The file was modified
src/HOL/MicroJava/DFA/Opt.thy
(diff)
The file was modified
src/HOL/MicroJava/DFA/Product.thy
(diff)
The file was modified
src/HOL/MicroJava/DFA/Semilat.thy
(diff)
The file was modified
src/HOL/MicroJava/DFA/SemilatAlg.thy
(diff)
The file was modified
src/HOL/MicroJava/DFA/Typing_Framework.thy
(diff)
The file was modified
src/HOL/MicroJava/J/Example.thy
(diff)
The file was modified
src/HOL/MicroJava/J/JBasis.thy
(diff)
The file was modified
src/HOL/MicroJava/J/TypeRel.thy
(diff)
The file was modified
src/HOL/MicroJava/J/WellForm.thy
(diff)
The file was modified
src/HOL/MicroJava/JVM/JVMExec.thy
(diff)
The file was modified
src/HOL/NanoJava/Equivalence.thy
(diff)
The file was modified
src/HOL/NanoJava/TypeRel.thy
(diff)
The file was modified
src/HOL/Nitpick_Examples/Core_Nits.thy
(diff)
The file was modified
src/HOL/Nitpick_Examples/Mini_Nits.thy
(diff)
The file was modified
src/HOL/Nitpick_Examples/Refute_Nits.thy
(diff)
The file was modified
src/HOL/Nominal/Examples/Class1.thy
(diff)
The file was modified
src/HOL/Nonstandard_Analysis/HyperDef.thy
(diff)
The file was modified
src/HOL/Nonstandard_Analysis/NSCA.thy
(diff)
The file was modified
src/HOL/Nonstandard_Analysis/Star.thy
(diff)
The file was modified
src/HOL/Predicate_Compile.thy
(diff)
The file was modified
src/HOL/Predicate_Compile_Examples/Hotel_Example.thy
(diff)
The file was modified
src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy
(diff)
The file was modified
src/HOL/Presburger.thy
(diff)
The file was modified
src/HOL/Prolog/Test.thy
(diff)
The file was modified
src/HOL/Prolog/Type.thy
(diff)
The file was modified
src/HOL/Proofs/Lambda/Commutation.thy
(diff)
The file was modified
src/HOL/Proofs/Lambda/Eta.thy
(diff)
The file was modified
src/HOL/Proofs/Lambda/InductTermi.thy
(diff)
The file was modified
src/HOL/Proofs/Lambda/Lambda.thy
(diff)
The file was modified
src/HOL/Proofs/Lambda/ListOrder.thy
(diff)
The file was modified
src/HOL/Proofs/Lambda/ParRed.thy
(diff)
The file was modified
src/HOL/Quickcheck_Examples/Hotel_Example.thy
(diff)
The file was modified
src/HOL/Quickcheck_Examples/Quickcheck_Examples.thy
(diff)
The file was modified
src/HOL/Quickcheck_Examples/Quickcheck_Narrowing_Examples.thy
(diff)
The file was modified
src/HOL/SET_Protocol/Cardholder_Registration.thy
(diff)
The file was modified
src/HOL/SET_Protocol/Event_SET.thy
(diff)
The file was modified
src/HOL/SET_Protocol/Merchant_Registration.thy
(diff)
The file was modified
src/HOL/SET_Protocol/Message_SET.thy
(diff)
The file was modified
src/HOL/SET_Protocol/Public_SET.thy
(diff)
The file was modified
src/HOL/SET_Protocol/Purchase.thy
(diff)
The file was modified
src/HOL/SMT_Examples/SMT_Examples.thy
(diff)
The file was modified
src/HOL/Set.thy
(diff)
The file was modified
src/HOL/Set_Interval.thy
(diff)
The file was modified
src/HOL/TLA/Memory/Memory.thy
(diff)
The file was modified
src/HOL/TLA/Memory/MemoryImplementation.thy
(diff)
The file was modified
src/HOL/TLA/Memory/MemoryParameters.thy
(diff)
The file was modified
src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML
(diff)
The file was modified
src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
(diff)
The file was modified
src/HOL/Transitive_Closure.thy
(diff)
The file was modified
src/HOL/UNITY/Comp/Alloc.thy
(diff)
The file was modified
src/HOL/UNITY/Comp/AllocBase.thy
(diff)
The file was modified
src/HOL/UNITY/Comp/Handshake.thy
(diff)
The file was modified
src/HOL/UNITY/Comp/Priority.thy
(diff)
The file was modified
src/HOL/UNITY/Comp/PriorityAux.thy
(diff)
The file was modified
src/HOL/UNITY/Comp/TimerArray.thy
(diff)
The file was modified
src/HOL/UNITY/Constrains.thy
(diff)
The file was modified
src/HOL/UNITY/ELT.thy
(diff)
The file was modified
src/HOL/UNITY/Extend.thy
(diff)
The file was modified
src/HOL/UNITY/FP.thy
(diff)
The file was modified
src/HOL/UNITY/Guar.thy
(diff)
The file was modified
src/HOL/UNITY/ListOrder.thy
(diff)
The file was modified
src/HOL/UNITY/PPROD.thy
(diff)
The file was modified
src/HOL/UNITY/Simple/NSP_Bad.thy
(diff)
The file was modified
src/HOL/UNITY/Simple/Reach.thy
(diff)
The file was modified
src/HOL/UNITY/Simple/Reachability.thy
(diff)
The file was modified
src/HOL/UNITY/SubstAx.thy
(diff)
The file was modified
src/HOL/UNITY/Transformers.thy
(diff)
The file was modified
src/HOL/UNITY/UNITY.thy
(diff)
The file was modified
src/HOL/UNITY/Union.thy
(diff)
The file was modified
src/HOL/UNITY/WFair.thy
(diff)
The file was modified
src/HOL/Word/Misc_Typedef.thy
(diff)
The file was modified
src/HOL/ZF/Games.thy
(diff)
The file was modified
src/HOL/ZF/HOLZF.thy
(diff)
The file was modified
src/HOL/ZF/LProd.thy
(diff)
The file was modified
src/HOL/ZF/Zet.thy
(diff)
The file was modified
src/HOL/Zorn.thy
(diff)
The file was modified
src/HOL/ex/Birthday_Paradox.thy
(diff)
The file was modified
src/HOL/ex/Dedekind_Real.thy
(diff)
The file was modified
src/HOL/ex/Executable_Relation.thy
(diff)
The file was modified
src/HOL/ex/Groebner_Examples.thy
(diff)
The file was modified
src/HOL/ex/Intuitionistic.thy
(diff)
The file was modified
src/HOL/ex/LocaleTest2.thy
(diff)
The file was modified
src/HOL/ex/Refute_Examples.thy
(diff)
The file was modified
src/HOL/ex/SAT_Examples.thy
(diff)
The file was modified
src/HOL/ex/Set_Comprehension_Pointfree_Examples.thy
(diff)
The file was modified
src/HOL/ex/Set_Theory.thy
(diff)
The file was modified
src/HOL/ex/Tarski.thy
(diff)
The file was modified
src/HOL/ex/While_Combinator_Example.thy
(diff)