HomeIsabelle/Phabricator
Diffusion Isabelle 89d05db6dd1f

Simplified, generalised version of Constructible due to E. Gunther, M. Pagano…
89d05db6dd1f
Actions

Description

Simplified, generalised version of Constructible due to E. Gunther, M. Pagano and P. Sánchez Terraf

Details

Provenance
paulson <lp15@cam.ac.uk>Authored on
Parents
rISABELLE6a1c1d1ce6ae: tuned
Branches
Unknown
Tags
Unknown

Changes (16)

PathSize
src/
ZF/
Constructible/

rISABELLE89d05db6dd1f

View Options

src/ZF/Constructible/AC_in_L.thy

Loading...
View Options

src/ZF/Constructible/DPow_absolute.thy

Loading...
View Options

src/ZF/Constructible/Datatype_absolute.thy

Loading...
View Options

src/ZF/Constructible/Formula.thy

Loading...
View Options

src/ZF/Constructible/Internalize.thy

Loading...
View Options

src/ZF/Constructible/L_axioms.thy

Loading...
View Options

src/ZF/Constructible/Normal.thy

Loading...
View Options

src/ZF/Constructible/Rank.thy

Loading...
View Options

src/ZF/Constructible/Rank_Separation.thy

Loading...
View Options

src/ZF/Constructible/Rec_Separation.thy

Loading...
View Options

src/ZF/Constructible/Reflection.thy

Loading...
View Options

src/ZF/Constructible/Relative.thy

Loading...
View Options

src/ZF/Constructible/Satisfies_absolute.thy

Loading...
View Options

src/ZF/Constructible/Separation.thy

Loading...
View Options

src/ZF/Constructible/WF_absolute.thy

Loading...
View Options

src/ZF/Constructible/Wellorderings.thy

Loading...