Diffusion afp-devel 80a3e62140de

generalized saturation framework theory a little, by using spurious 'Q' as a…
80a3e62140de
Actions

Tags

None

Subscribers

None

Description

generalized saturation framework theory a little, by using spurious 'Q' as a set (with Sophie Tourret's permission)

Details

Provenance

Authored on

Parents

rAFP882b6b02de94: corrected classification

Branches

Unknown

Tags

Unknown

Event Timeline

blanchette committed rAFP80a3e62140de: generalized saturation framework theory a little, by using spurious 'Q' as a….Apr 28 2020, 5:20 PM

Changes (5)

Path

Size

thys/

Saturation_Framework/

Consequence_Relations_and_Inference_Systems.thy

Labeled_Lifting_to_Non_Ground_Calculi.thy

Lifting_to_Non_Ground_Calculi.thy

Prover_Architectures.thy

rAFP80a3e62140de

thys/Saturation_Framework/Calculi.thy

Loading...

thys/Saturation_Framework/Consequence_Relations_and_Inference_Systems.thy

Loading...

thys/Saturation_Framework/Labeled_Lifting_to_Non_Ground_Calculi.thy

Loading...

thys/Saturation_Framework/Lifting_to_Non_Ground_Calculi.thy

Loading...

thys/Saturation_Framework/Prover_Architectures.thy

Loading...