Skip to content
Success

Changes

Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

Summary

  1. Further reduction of locale assumptions
Changeset 12905:a0a812d549dd by sterraf:
Further reduction of locale assumptions
The file was addedthys/Transitive_Models/Relativization.ml
The file was addedthys/Transitive_Models/Synthetic_Definition.ml
The file was modified thys/Delta_System_Lemma/Cardinal_Library.thy
The file was modified thys/Delta_System_Lemma/ZF_Library.thy
The file was modified thys/Independence_CH/CH.thy
The file was modified thys/Independence_CH/Cardinal_Preservation.thy
The file was modified thys/Independence_CH/Choice_Axiom.thy
The file was modified thys/Independence_CH/Cohen_Posets_Relative.thy
The file was modified thys/Independence_CH/Definitions_Main.thy
The file was modified thys/Independence_CH/Fm_Definitions.thy
The file was modified thys/Independence_CH/Forces_Definition.thy
The file was modified thys/Independence_CH/Forcing_Data.thy
The file was modified thys/Independence_CH/Forcing_Main.thy
The file was modified thys/Independence_CH/Forcing_Notions.thy
The file was modified thys/Independence_CH/Forcing_Theorems.thy
The file was modified thys/Independence_CH/Interface.thy
The file was modified thys/Independence_CH/Kappa_Closed_Notions.thy
The file was modified thys/Independence_CH/Not_CH.thy
The file was modified thys/Independence_CH/Proper_Extension.thy
The file was modified thys/Independence_CH/Replacement_Axiom.thy
The file was modified thys/Independence_CH/Replacement_Instances.thy
The file was modified thys/Independence_CH/Separation_Axiom.thy
The file was modified thys/Independence_CH/Separation_Instances.thy
The file was modified thys/Independence_CH/Union_Axiom.thy
The file was modified thys/Independence_CH/ZF_Trans_Interpretations.thy
The file was modified thys/Transitive_Models/CardinalArith_Relative.thy
The file was modified thys/Transitive_Models/Cardinal_AC_Relative.thy
The file was modified thys/Transitive_Models/Cardinal_Library_Relative.thy
The file was modified thys/Transitive_Models/Cardinal_Relative.thy
The file was modified thys/Transitive_Models/Delta_System_Relative.thy
The file was modified thys/Transitive_Models/Discipline_Base.thy
The file was modified thys/Transitive_Models/Discipline_Cardinal.thy
The file was modified thys/Transitive_Models/Discipline_Function.thy
The file was modified thys/Transitive_Models/Higher_Order_Constructs.thy
The file was modified thys/Transitive_Models/Lambda_Replacement.thy
The file was modified thys/Transitive_Models/Least.thy
The file was modified thys/Transitive_Models/M_Basic_No_Repl.thy
The file was modified thys/Transitive_Models/Partial_Functions_Relative.thy
The file was modified thys/Transitive_Models/Pointed_DC_Relative.thy
The file was modified thys/Transitive_Models/Recursion_Thms.thy
The file was modified thys/Transitive_Models/Relativization.thy
The file was modified thys/Transitive_Models/Renaming_Auto.thy
The file was modified thys/Transitive_Models/Renaming_ML.ml
The file was modified thys/Transitive_Models/Synthetic_Definition.thy
The file was modified thys/Transitive_Models/ZF_Library_Relative.thy
The file was modified thys/Transitive_Models/ZF_Miscellanea.thy
The file was modified thys/Transitive_Models/document/root.bib
The file was modified thys/Transitive_Models/document/root.tex