![[Jenkins]](/jenkins/static/77e8e0f1/images/svgs/logo.svg){kind=logo}
Summary
- disable export_document by default (presently unused and for demo/testing purposes): avoid spurious IO exception in highly parallel environment;
- simplified ZF theory names (in contrast to 6a0801279f4c): session-qualification already achieves disjointness;
- merged
- more modernisaton and de-applying
| The file was modified | etc/options (diff) |
| The file was modified | src/Pure/Thy/thy_info.ML (diff) |
| The file was modified | src/Pure/Tools/dump.scala (diff) |
| The file was added | src/ZF/Datatype.thy |
| The file was added | src/ZF/Inductive.thy |
| The file was added | src/ZF/Int.thy |
| The file was added | src/ZF/IntDiv.thy |
| The file was added | src/ZF/List.thy |
| The file was added | src/ZF/Nat.thy |
| The file was modified | src/ZF/Bin.thy (diff) |
| The file was modified | src/ZF/Cardinal.thy (diff) |
| The file was modified | src/ZF/Epsilon.thy (diff) |
| The file was modified | src/ZF/Finite.thy (diff) |
| The file was modified | src/ZF/Induct/Tree_Forest.thy (diff) |
| The file was modified | src/ZF/InfDatatype.thy (diff) |
| The file was modified | src/ZF/OrderType.thy (diff) |
| The file was modified | src/ZF/ZF.thy (diff) |
| The file was modified | src/ZF/Zorn.thy (diff) |
| The file was removed | src/ZF/Datatype_ZF.thy |
| The file was removed | src/ZF/Inductive_ZF.thy |
| The file was removed | src/ZF/IntDiv_ZF.thy |
| The file was removed | src/ZF/Int_ZF.thy |
| The file was removed | src/ZF/List_ZF.thy |
| The file was removed | src/ZF/Nat_ZF.thy |
| The file was modified | src/HOL/Algebra/Complete_Lattice.thy (diff) |
| The file was modified | src/HOL/Algebra/Divisibility.thy (diff) |
| The file was modified | src/HOL/Algebra/Sylow.thy (diff) |