HomeIsabelle/Phabricator
Diffusion afp-devel a51be9ca4b87

updated, replacing axiomatizations by proper locales
a51be9ca4b87
Actions

Description

updated, replacing axiomatizations by proper locales

Details

Provenance
paulson <lp15@cam.ac.uk>Authored on
Parents
rAFPfd98855f4f8e: bundles for traditional infix syntax
Branches
Unknown
Tags
Unknown

Changes (11)

PathSize
thys/
Projective_Geometry/

rAFPa51be9ca4b87

View Options

thys/Projective_Geometry/Desargues_2D.thy

Loading...
View Options

thys/Projective_Geometry/Desargues_3D.thy

Loading...
View Options

thys/Projective_Geometry/Desargues_Property.thy

Loading...
View Options

thys/Projective_Geometry/Higher_Projective_Space_Axioms.thy

Loading...
View Options

thys/Projective_Geometry/Higher_Projective_Space_Rank_Axioms.thy

Loading...
View Options

thys/Projective_Geometry/Matroid_Rank_Properties.thy

Loading...
View Options

thys/Projective_Geometry/Pappus_Desargues.thy

Loading...
View Options

thys/Projective_Geometry/Pappus_Property.thy

Loading...
View Options

thys/Projective_Geometry/Pascal_Property.thy

Loading...
View Options

thys/Projective_Geometry/Projective_Plane_Axioms.thy

Loading...
View Options

thys/Projective_Geometry/Projective_Space_Axioms.thy

Loading...