Diffusion afp-devel 1b0a95af1620

avoid noncanonical uses of 'moura' tactic ahead of new implementation of tactic
1b0a95af1620
Actions

Tags

None

Subscribers

None

Description

avoid noncanonical uses of 'moura' tactic ahead of new implementation of tactic

Details

Provenance

Authored on

Parents

rAFP72cce11020f9: tuned proofs

Branches

Unknown

Tags

Unknown

Event Timeline

blanchette committed rAFP1b0a95af1620: avoid noncanonical uses of 'moura' tactic ahead of new implementation of tactic.Feb 20 2024, 9:15 AM

Changes (23)

Path

Size

thys/

Chandy_Lamport/

Distributed_System.thy

CryptHOL/

Misc_CryptHOL.thy

DiscretePricing/

Factored_Transition_System_Bounding/

HOLCF-Prelude/

examples/

Sieve_Primes.thy

IsaGeoCoq/

Tarski_Neutral.thy

Lp/

Functional_Spaces.thy

Multi_Party_Computation/

Uniform_Sampling.thy

Stateful_Protocol_Composition_and_Typing/

Intruder_Deduction.thy

Labeled_Stateful_Strands.thy

Labeled_Strands.thy

Lazy_Intruder.thy

Miscellaneous.thy

More_Unification.thy

Parallel_Compositionality.thy

Stateful_Compositionality.thy

Stateful_Strands.thy

Stateful_Typing.thy

Strands_and_Constraints.thy

Typed_Model.thy

Typing_Result.thy

rAFP1b0a95af1620

thys/Chandy_Lamport/Distributed_System.thy

Loading...

thys/Chandy_Lamport/Util.thy

Loading...

thys/CryptHOL/Misc_CryptHOL.thy

Loading...

thys/DiscretePricing/CRR_Model.thy

Loading...

thys/DiscretePricing/Fair_Price.thy

Loading...

thys/Factored_Transition_System_Bounding/Dependency.thy

Loading...

thys/HOLCF-Prelude/examples/Sieve_Primes.thy

Loading...

thys/IsaGeoCoq/Tarski_Neutral.thy

Loading...

thys/Lp/Functional_Spaces.thy

Loading...

thys/Multi_Party_Computation/Uniform_Sampling.thy

Loading...

thys/Stateful_Protocol_Composition_and_Typing/Intruder_Deduction.thy

Loading...

thys/Stateful_Protocol_Composition_and_Typing/Labeled_Stateful_Strands.thy

Loading...

thys/Stateful_Protocol_Composition_and_Typing/Labeled_Strands.thy

Loading...

thys/Stateful_Protocol_Composition_and_Typing/Lazy_Intruder.thy

Loading...

thys/Stateful_Protocol_Composition_and_Typing/Miscellaneous.thy

Loading...

thys/Stateful_Protocol_Composition_and_Typing/More_Unification.thy

Loading...

thys/Stateful_Protocol_Composition_and_Typing/Parallel_Compositionality.thy

Loading...

thys/Stateful_Protocol_Composition_and_Typing/Stateful_Compositionality.thy

Loading...

thys/Stateful_Protocol_Composition_and_Typing/Stateful_Strands.thy

Loading...

thys/Stateful_Protocol_Composition_and_Typing/Stateful_Typing.thy

Loading...

thys/Stateful_Protocol_Composition_and_Typing/Strands_and_Constraints.thy

Loading...

thys/Stateful_Protocol_Composition_and_Typing/Typed_Model.thy

Loading...

thys/Stateful_Protocol_Composition_and_Typing/Typing_Result.thy

Loading...