Diffusion afp-devel a0a812d549dd

Further reduction of locale assumptions
a0a812d549dd
Actions

Tags

None

Subscribers

None

Description

Further reduction of locale assumptions

Details

Provenance

Authored on

Parents

rAFP41e138072234: merged

Branches

Unknown

Tags

Unknown

Event Timeline

sterraf committed rAFPa0a812d549dd: Further reduction of locale assumptions.Aug 9 2022, 5:59 PM

Changes (50)

Path

Size

Delta_System_Lemma/

Cardinal_Library.thy

Independence_CH/

Cardinal_Preservation.thy

Choice_Axiom.thy

Cohen_Posets_Relative.thy

Definitions_Main.thy

Fm_Definitions.thy

Forces_Definition.thy

Forcing_Data.thy

Forcing_Main.thy

Forcing_Notions.thy

Forcing_Theorems.thy

Kappa_Closed_Notions.thy

Proper_Extension.thy

Replacement_Axiom.thy

Replacement_Instances.thy

Separation_Axiom.thy

Separation_Instances.thy

Union_Axiom.thy

ZF_Trans_Interpretations.thy

Transitive_Models

CardinalArith_Relative.thy

Cardinal_AC_Relative.thy

Cardinal_Library_Relative.thy

Cardinal_Relative.thy

Delta_System_Relative.thy

Discipline_Base.thy

Discipline_Cardinal.thy

Discipline_Function.thy

Higher_Order_Constructs.thy

Lambda_Replacement.thy

M_Basic_No_Repl.thy

Partial_Functions_Relative.thy

Pointed_DC_Relative.thy

Recursion_Thms.thy

Relativization.ml

Relativization.thy

Renaming_Auto.thy

Synthetic_Definition.ml

Synthetic_Definition.thy

ZF_Library_Relative.thy

ZF_Miscellanea.thy

document/

rAFPa0a812d549dd

thys/Delta_System_Lemma/Cardinal_Library.thy

Loading...

thys/Delta_System_Lemma/ZF_Library.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/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/Interface.thy

Loading...

thys/Independence_CH/Kappa_Closed_Notions.thy

Loading...

thys/Independence_CH/Not_CH.thy

Loading...

thys/Independence_CH/Proper_Extension.thy

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/Union_Axiom.thy

Loading...

thys/Independence_CH/ZF_Trans_Interpretations.thy

Loading...

thys/Transitive_Models/CardinalArith_Relative.thy

Loading...

thys/Transitive_Models/Cardinal_AC_Relative.thy

Loading...

thys/Transitive_Models/Cardinal_Library_Relative.thy

Loading...

thys/Transitive_Models/Cardinal_Relative.thy

Loading...

thys/Transitive_Models/Delta_System_Relative.thy

Loading...

thys/Transitive_Models/Discipline_Base.thy

Loading...

thys/Transitive_Models/Discipline_Cardinal.thy

Loading...

thys/Transitive_Models/Discipline_Function.thy

Loading...

thys/Transitive_Models/Higher_Order_Constructs.thy

Loading...

thys/Transitive_Models/Lambda_Replacement.thy

Loading...

thys/Transitive_Models/Least.thy

Loading...

thys/Transitive_Models/M_Basic_No_Repl.thy

Loading...

thys/Transitive_Models/Partial_Functions_Relative.thy

Loading...

thys/Transitive_Models/Pointed_DC_Relative.thy

Loading...

thys/Transitive_Models/Recursion_Thms.thy

Loading...

thys/Transitive_Models/Relativization.ml

Loading...

thys/Transitive_Models/Relativization.thy

Loading...

thys/Transitive_Models/Renaming_Auto.thy

Loading...

thys/Transitive_Models/Renaming_ML.ml

Loading...

thys/Transitive_Models/Synthetic_Definition.ml

Loading...

thys/Transitive_Models/Synthetic_Definition.thy

Loading...

thys/Transitive_Models/ZF_Library_Relative.thy

Loading...

thys/Transitive_Models/ZF_Miscellanea.thy

Loading...

thys/Transitive_Models/document/root.bib

Loading...

thys/Transitive_Models/document/root.tex

Loading...