Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. merged
  2. added lemmas wf_imp_asym, wfP_imp_asymp, and wfP_imp_irreflp
  3. removed $ite from E 2.6 in THF format
  4. New and simplified theorems
  5. merged
  6. prefixed all mirabelle_sledgehammer output lines with sledgehammer output
Changeset 74972:e578640c787a by desharna:
merged
Changeset 74971:16eaa56f69f7 by desharna:
added lemmas wf_imp_asym, wfP_imp_asymp, and wfP_imp_irreflp
The file was modified src/HOL/Wellfounded.thy
Changeset 74970:afd8da649d75 by desharna:
removed $ite from E 2.6 in THF format
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
Changeset 74969:fa0020b47868 by paulson _lp15@cam.ac.uk_:
New and simplified theorems
The file was modified src/HOL/Analysis/Derivative.thy
The file was modified src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy
The file was modified src/HOL/Factorial.thy
The file was modified src/HOL/Set_Interval.thy
Changeset 74968:507203e30db4 by desharna:
merged
Changeset 74967:3f55c5feca58 by desharna:
prefixed all mirabelle_sledgehammer output lines with sledgehammer output
The file was modified src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML

Summary

  1. CS: possibility to disable backtracking; CZH: auxiliary results; ETTS: minor amendments
  2. used wfP_imp_asymp from HOL
  3. simplified proof some more
  4. simplified proof
  5. Extended protocol model to support composition of more than two protocols without the need of re-labeling them, additional automated checks, tighter integration of the stateful protocol model and the automated verification (PSPSP) tool.
Changeset 12330:241da1cdeabf by user9716869 _user9716869@gmail.com_:
CS: possibility to disable backtracking; CZH: auxiliary results; ETTS: minor amendments
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_DG_FUNCT.thy
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_CSimplicial.thy
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Category.thy
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Comma.thy
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Discrete.thy
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_FUNCT.thy
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Functor.thy
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Hom.thy
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_NTCF.thy
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Order.thy
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Ordinal.thy
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_PCategory.thy
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Par.thy
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Parallel.thy
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Rel.thy
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_SS.thy
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Set.thy
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Simple.thy
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Small_Category.thy
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Small_Functor.thy
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Small_NTCF.thy
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Structure_Example.thy
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Subcategory.thy
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_ECAT_Yoneda.thy
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_SMC_CAT.thy
The file was modified thys/CZH_Elementary_Categories/czh_ecategories/CZH_SMC_FUNCT.thy
The file was modified thys/CZH_Foundations/czh_digraphs/CZH_DG_DGHM.thy
The file was modified thys/CZH_Foundations/czh_digraphs/CZH_DG_Digraph.thy
The file was modified thys/CZH_Foundations/czh_digraphs/CZH_DG_Introduction.thy
The file was modified thys/CZH_Foundations/czh_digraphs/CZH_DG_PDigraph.thy
The file was modified thys/CZH_Foundations/czh_digraphs/CZH_DG_Rel.thy
The file was modified thys/CZH_Foundations/czh_digraphs/CZH_DG_Simple.thy
The file was modified thys/CZH_Foundations/czh_digraphs/CZH_DG_Small_DGHM.thy
The file was modified thys/CZH_Foundations/czh_digraphs/CZH_DG_Small_Digraph.thy
The file was modified thys/CZH_Foundations/czh_digraphs/CZH_DG_Small_TDGHM.thy
The file was modified thys/CZH_Foundations/czh_digraphs/CZH_DG_Subdigraph.thy
The file was modified thys/CZH_Foundations/czh_digraphs/CZH_DG_TDGHM.thy
The file was modified thys/CZH_Foundations/czh_introduction/CZH_Introduction.thy
The file was modified thys/CZH_Foundations/czh_semicategories/CZH_SMC_GRPH.thy
The file was modified thys/CZH_Foundations/czh_semicategories/CZH_SMC_NTSMCF.thy
The file was modified thys/CZH_Foundations/czh_semicategories/CZH_SMC_PSemicategory.thy
The file was modified thys/CZH_Foundations/czh_semicategories/CZH_SMC_Par.thy
The file was modified thys/CZH_Foundations/czh_semicategories/CZH_SMC_Rel.thy
The file was modified thys/CZH_Foundations/czh_semicategories/CZH_SMC_SemiCAT.thy
The file was modified thys/CZH_Foundations/czh_semicategories/CZH_SMC_Semicategory.thy
The file was modified thys/CZH_Foundations/czh_semicategories/CZH_SMC_Semifunctor.thy
The file was modified thys/CZH_Foundations/czh_semicategories/CZH_SMC_Set.thy
The file was modified thys/CZH_Foundations/czh_semicategories/CZH_SMC_Simple.thy
The file was modified thys/CZH_Foundations/czh_semicategories/CZH_SMC_Small_NTSMCF.thy
The file was modified thys/CZH_Foundations/czh_semicategories/CZH_SMC_Small_Semicategory.thy
The file was modified thys/CZH_Foundations/czh_semicategories/CZH_SMC_Small_Semifunctor.thy
The file was modified thys/CZH_Foundations/czh_semicategories/CZH_SMC_Subsemicategory.thy
The file was modified thys/CZH_Foundations/czh_sets/CZH_Sets_BRelations.thy
The file was modified thys/CZH_Foundations/czh_sets/CZH_Sets_NOP.thy
The file was modified thys/CZH_Foundations/czh_sets/CZH_Sets_Nat.thy
The file was modified thys/CZH_Foundations/czh_sets/CZH_Sets_VNHS.thy
The file was modified thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Adjoints.thy
The file was modified thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Complete.thy
The file was modified thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Kan.thy
The file was modified thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Limit.thy
The file was modified thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_PWKan.thy
The file was modified thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_PWKan_Example.thy
The file was modified thys/CZH_Universal_Constructions/czh_ucategories/CZH_UCAT_Universal.thy
The file was modified thys/CZH_Universal_Constructions/document/root.bib
The file was modified thys/Conditional_Simplification/CS_Cond_Simp.ML
The file was modified thys/Conditional_Simplification/CS_Reference.thy
The file was modified thys/Conditional_Simplification/CS_UM.ML
The file was modified thys/Conditional_Simplification/IHOL_CS.thy
The file was modified thys/Types_To_Sets_Extension/Examples/SML_Relativization/Topology/SML_Product_Topology.thy
The file was modified thys/Types_To_Sets_Extension/Examples/SML_Relativization/Topology/SML_Topological_Space.thy
Changeset 12329:c55c666012a3 by desharna:
used wfP_imp_asymp from HOL
The file was modified thys/Saturation_Framework_Extensions/Standard_Redundancy_Criterion.thy
Changeset 12328:cae2c55e7bbb by desharna:
simplified proof some more
The file was modified thys/Saturation_Framework_Extensions/Standard_Redundancy_Criterion.thy
Changeset 12327:1d3873e125b1 by desharna:
simplified proof
The file was modified thys/Saturation_Framework_Extensions/Standard_Redundancy_Criterion.thy
Changeset 12326:66d4e5d44d29 by achim d. brucker _adbrucker@0x5f.org_:
Extended protocol model to support composition of more than two protocols without<br>the need of re-labeling them, additional automated checks, tighter integration<br>of the stateful protocol model and the automated verification (PSPSP) tool.
The file was addedthys/Automated_Stateful_Protocol_Verification/PSPSP-Manual/KeyserverEx.thy
The file was addedthys/Automated_Stateful_Protocol_Verification/PSPSP-Manual/introduction.thy
The file was addedthys/Automated_Stateful_Protocol_Verification/PSPSP-Manual/manual.thy
The file was addedthys/Automated_Stateful_Protocol_Verification/document/jedit-keyserver.png
The file was addedthys/Automated_Stateful_Protocol_Verification/document/jedit-select-session.png
The file was addedthys/Automated_Stateful_Protocol_Verification/document/lh-listings.sty
The file was modified thys/Automated_Stateful_Protocol_Verification/Eisbach_Protocol_Verification.thy
The file was modified thys/Automated_Stateful_Protocol_Verification/Examples.thy
The file was modified thys/Automated_Stateful_Protocol_Verification/PSPSP.thy
The file was modified thys/Automated_Stateful_Protocol_Verification/ROOT
The file was modified thys/Automated_Stateful_Protocol_Verification/Stateful_Protocol_Model.thy
The file was modified thys/Automated_Stateful_Protocol_Verification/Stateful_Protocol_Verification.thy
The file was modified thys/Automated_Stateful_Protocol_Verification/Term_Abstraction.thy
The file was modified thys/Automated_Stateful_Protocol_Verification/Term_Implication.thy
The file was modified thys/Automated_Stateful_Protocol_Verification/Term_Variants.thy
The file was modified thys/Automated_Stateful_Protocol_Verification/Transactions.thy
The file was modified thys/Automated_Stateful_Protocol_Verification/document/root.bib
The file was modified thys/Automated_Stateful_Protocol_Verification/document/root.tex
The file was modified thys/Automated_Stateful_Protocol_Verification/examples/Keyserver.thy
The file was modified thys/Automated_Stateful_Protocol_Verification/examples/Keyserver2.thy
The file was modified thys/Automated_Stateful_Protocol_Verification/examples/Keyserver_Composition.thy
The file was modified thys/Automated_Stateful_Protocol_Verification/examples/PKCS/PKCS_Model03.thy
The file was modified thys/Automated_Stateful_Protocol_Verification/examples/PKCS/PKCS_Model07.thy
The file was modified thys/Automated_Stateful_Protocol_Verification/examples/PKCS/PKCS_Model09.thy
The file was modified thys/Automated_Stateful_Protocol_Verification/trac/Makefile
The file was modified thys/Automated_Stateful_Protocol_Verification/trac/bin/ml-lex-isa
The file was modified thys/Automated_Stateful_Protocol_Verification/trac/bin/ml-yacc-isa
The file was modified thys/Automated_Stateful_Protocol_Verification/trac/ml_yacc_lib.thy
The file was modified thys/Automated_Stateful_Protocol_Verification/trac/trac.thy
The file was modified thys/Automated_Stateful_Protocol_Verification/trac/trac_fp_parser.thy
The file was modified thys/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_fp.grm
The file was modified thys/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_fp.grm.sml
The file was modified thys/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_fp.lex
The file was modified thys/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_fp.lex.sml
The file was modified thys/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_protocol.grm
The file was modified thys/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_protocol.grm.sig
The file was modified thys/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_protocol.grm.sml
The file was modified thys/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_protocol.lex
The file was modified thys/Automated_Stateful_Protocol_Verification/trac/trac_parser/trac_protocol.lex.sml
The file was modified thys/Automated_Stateful_Protocol_Verification/trac/trac_protocol_parser.thy
The file was modified thys/Automated_Stateful_Protocol_Verification/trac/trac_term.thy
The file was modified thys/Stateful_Protocol_Composition_and_Typing/Examples.thy
The file was modified thys/Stateful_Protocol_Composition_and_Typing/Intruder_Deduction.thy
The file was modified thys/Stateful_Protocol_Composition_and_Typing/Labeled_Stateful_Strands.thy
The file was modified thys/Stateful_Protocol_Composition_and_Typing/Labeled_Strands.thy
The file was modified thys/Stateful_Protocol_Composition_and_Typing/Lazy_Intruder.thy
The file was modified thys/Stateful_Protocol_Composition_and_Typing/Messages.thy
The file was modified thys/Stateful_Protocol_Composition_and_Typing/Miscellaneous.thy
The file was modified thys/Stateful_Protocol_Composition_and_Typing/More_Unification.thy
The file was modified thys/Stateful_Protocol_Composition_and_Typing/Parallel_Compositionality.thy
The file was modified thys/Stateful_Protocol_Composition_and_Typing/ROOT
The file was modified thys/Stateful_Protocol_Composition_and_Typing/Stateful_Compositionality.thy
The file was modified thys/Stateful_Protocol_Composition_and_Typing/Stateful_Strands.thy
The file was modified thys/Stateful_Protocol_Composition_and_Typing/Stateful_Typing.thy
The file was modified thys/Stateful_Protocol_Composition_and_Typing/Strands_and_Constraints.thy
The file was modified thys/Stateful_Protocol_Composition_and_Typing/Typed_Model.thy
The file was modified thys/Stateful_Protocol_Composition_and_Typing/Typing_Result.thy
The file was modified thys/Stateful_Protocol_Composition_and_Typing/document/root.tex
The file was modified thys/Stateful_Protocol_Composition_and_Typing/examples/Example_Keyserver.thy
The file was modified thys/Stateful_Protocol_Composition_and_Typing/examples/Example_TLS.thy