Diffusion afp-devel 9cc7791da210

added 'sublocale', simplified rest of formalization
9cc7791da210
Actions

Tags

None

Subscribers

None

Description

added 'sublocale', simplified rest of formalization

Details

Provenance

Authored on

Parents

rAFPec19eb9df9f6: tuned topics

Branches

Unknown

Tags

Unknown

Event Timeline

blanchette committed rAFP9cc7791da210: added 'sublocale', simplified rest of formalization.May 8 2020, 5:49 PM

Changes (3)

Path

Size

thys/

Saturation_Framework/

Consequence_Relations_and_Inference_Systems.thy

Labeled_Lifting_to_Non_Ground_Calculi.thy

Prover_Architectures.thy

rAFP9cc7791da210

thys/Saturation_Framework/Consequence_Relations_and_Inference_Systems.thy

Loading...

thys/Saturation_Framework/Labeled_Lifting_to_Non_Ground_Calculi.thy

Loading...

thys/Saturation_Framework/Prover_Architectures.thy

Loading...