Diffusion afp-devel f0c701e6661f

new entry Independence_CH
f0c701e6661f
Actions

Tags

None

Subscribers

None

Description

new entry Independence_CH

Details

Provenance

paulson <lp15@cam.ac.uk>

Authored on

Parents

rAFPbf120ce6a2ff: New entry ResiduatedTransitionSystem

Branches

Unknown

Tags

Unknown

Event Timeline

paulson <lp15@cam.ac.uk> committed rAFPf0c701e6661f: new entry Independence_CH.Mar 7 2022, 2:53 PM

Changes (44)

Path

Size

Independence_CH

Absolute_Versions.thy

Cardinal_Preservation.thy

Choice_Axiom.thy

Cohen_Posets_Relative.thy

Definitions_Main.thy

Demonstrations.thy

Extensionality_Axiom.thy

Fm_Definitions.thy

Forces_Definition.thy

Forcing_Data.thy

Forcing_Main.thy

Forcing_Notions.thy

Forcing_Theorems.thy

Foundation_Axiom.thy

FrecR_Arities.thy

Infinity_Axiom.thy

Internal_ZFC_Axioms.thy

Kappa_Closed_Notions.thy

Ordinals_In_MG.thy

Pairing_Axiom.thy

Powerset_Axiom.thy

Proper_Extension.thy

Replacement_Axiom.thy

Replacement_Instances.thy

Separation_Axiom.thy

Separation_Instances.thy

Separation_Rename.thy

Succession_Poset.thy

Union_Axiom.thy

ZF_Trans_Interpretations.thy

rAFPf0c701e6661f

thys/Independence_CH/Absolute_Versions.thy

Loading...

thys/Independence_CH/CH.thy

Loading...

thys/Independence_CH/Cardinal_Preservation.thy

Loading...

thys/Independence_CH/Choice_Axiom.thy

Loading...

thys/Independence_CH/Cohen_Posets_Relative.thy

Loading...

thys/Independence_CH/Definitions_Main.thy

Loading...

thys/Independence_CH/Demonstrations.thy

Loading...

thys/Independence_CH/Edrel.thy

Loading...

thys/Independence_CH/Extensionality_Axiom.thy

Loading...

thys/Independence_CH/Fm_Definitions.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/Foundation_Axiom.thy

Loading...

thys/Independence_CH/FrecR.thy

Loading...

thys/Independence_CH/FrecR_Arities.thy

Loading...

thys/Independence_CH/Infinity_Axiom.thy

Loading...

thys/Independence_CH/Interface.thy

Loading...

thys/Independence_CH/Internal_ZFC_Axioms.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/Ordinals_In_MG.thy

Loading...

thys/Independence_CH/Pairing_Axiom.thy

Loading...

thys/Independence_CH/Powerset_Axiom.thy

Loading...

thys/Independence_CH/Proper_Extension.thy

Loading...

thys/Independence_CH/ROOT

Loading...

thys/Independence_CH/Replacement_Axiom.thy

Loading...

thys/Independence_CH/Replacement_Instances.thy

Loading...

thys/Independence_CH/Separation_Axiom.thy

Loading...

thys/Independence_CH/Separation_Instances.thy

Loading...

thys/Independence_CH/Separation_Rename.thy

Loading...

thys/Independence_CH/Succession_Poset.thy

Loading...

thys/Independence_CH/Union_Axiom.thy

Loading...

thys/Independence_CH/ZF_Trans_Interpretations.thy

Loading...

thys/Independence_CH/document/root.bib

Loading...

thys/Independence_CH/document/root.bst

Loading...

thys/Independence_CH/document/root.tex

Loading...

thys/ROOTS

Loading...