HomeIsabelle/Phabricator
Diffusion afp-devel 3f6499d19e84

simplified proof using Uwe Waldmann's idea + tuning
3f6499d19e84
Actions

Description

simplified proof using Uwe Waldmann's idea + tuning

Details

Provenance
blanchetteAuthored on
Parents
rAFP558943ac6e3d: tuned
Branches
Unknown
Tags
Unknown

Changes (4)

PathSize
thys/
Saturation_Framework/
Saturation_Framework_Extensions/

rAFP3f6499d19e84

View Options

thys/Saturation_Framework/Given_Clause_Architectures.thy

Loading...
View Options

thys/Saturation_Framework_Extensions/Clausal_Calculus.thy

Loading...
View Options

thys/Saturation_Framework_Extensions/FO_Ordered_Resolution_Prover_Revisited.thy

Loading...
View Options

thys/Saturation_Framework_Extensions/Soundness.thy

Loading...