Diffusion afp-devel 93b0051abb90

Revised locale structure and notation. Proposed modularization for ZF…
93b0051abb90
Actions

Tags

None

Subscribers

None

Description

Revised locale structure and notation. Proposed modularization for ZF-Constructible's M_eclose

Details

Provenance

Authored on

Parents

rAFP358ee38a13a3: tuning

Branches

Unknown

Tags

Unknown

Event Timeline

sterraf committed rAFP93b0051abb90: Revised locale structure and notation. Proposed modularization for ZF….Aug 25 2022, 4:45 PM

Changes (29)

Path

Size

Independence_CH/

Cardinal_Preservation.thy

Choice_Axiom.thy

Definitions_Main.thy

Forces_Definition.thy

Forcing_Data.thy

Forcing_Main.thy

Forcing_Notions.thy

Forcing_Theorems.thy

Kappa_Closed_Notions.thy

Powerset_Axiom.thy

Proper_Extension.thy

Replacement_Axiom.thy

Separation_Axiom.thy

Union_Axiom.thy

ZF_Trans_Interpretations.thy

Transitive_Models

DPow_absolute.thy

Datatype_absolute.thy

Eclose_Absolute.thy

Internalizations.thy

Internalize.thy

Rec_Separation.thy

Recursion_Thms.thy

Relativization.thy

Satisfies_absolute.thy

rAFP93b0051abb90

thys/Independence_CH/Cardinal_Preservation.thy

Loading...

thys/Independence_CH/Choice_Axiom.thy

Loading...

thys/Independence_CH/Definitions_Main.thy

Loading...

thys/Independence_CH/Forces_Definition.thy

Loading...

thys/Independence_CH/Forcing_Data.thy

Loading...

thys/Independence_CH/Forcing_Main.thy

Loading...

thys/Independence_CH/Forcing_Notions.thy

Loading...

thys/Independence_CH/Forcing_Theorems.thy

Loading...

thys/Independence_CH/Interface.thy

Loading...

thys/Independence_CH/Kappa_Closed_Notions.thy

Loading...

thys/Independence_CH/Names.thy

Loading...

thys/Independence_CH/Not_CH.thy

Loading...

thys/Independence_CH/Powerset_Axiom.thy

Loading...

thys/Independence_CH/Proper_Extension.thy

Loading...

thys/Independence_CH/Replacement_Axiom.thy

Loading...

thys/Independence_CH/Separation_Axiom.thy

Loading...

thys/Independence_CH/Union_Axiom.thy

Loading...

thys/Independence_CH/ZF_Trans_Interpretations.thy

Loading...

thys/Transitive_Models/DPow_absolute.thy

Loading...

thys/Transitive_Models/Datatype_absolute.thy

Loading...

thys/Transitive_Models/Eclose_Absolute.thy

Loading...

thys/Transitive_Models/Internalizations.thy

Loading...

thys/Transitive_Models/Internalize.thy

Loading...

thys/Transitive_Models/Rec_Separation.thy

Loading...

thys/Transitive_Models/Recursion_Thms.thy

Loading...

thys/Transitive_Models/Relativization.thy

Loading...

thys/Transitive_Models/Satisfies_absolute.thy

Loading...