Diffusion Isabelle 0c18df79b1c8

more modernisation of syntax
0c18df79b1c8
Actions

Tags

None

Subscribers

None

Description

more modernisation of syntax

Details

Provenance

paulson <lp15@cam.ac.uk>

Authored on

Parents

rISABELLEe44d86131648: Removal of obsolete ASCII syntax

Branches

Unknown

Tags

Unknown

Event Timeline

paulson <lp15@cam.ac.uk> committed rISABELLE0c18df79b1c8: more modernisation of syntax.Sep 27 2022, 6:03 PM

makarius mentioned this in rISABELLEcf7db6353322: recover informal "&" from 0c18df79b1c8;.Sep 28 2022, 12:24 PM

Changes (105)
Show All Changes

Very Large Commit

This commit is very large. Load each file individually.

Path

Size

src/

ZF/

AC/

AC16_lemmas.thy

Cardinal_aux.thy

CardinalArith.thy

Coind/

Constructible/

DPow_absolute.thy

Datatype_absolute.thy

Internalize.thy

Rank_Separation.thy

Rec_Separation.thy

Satisfies_absolute.thy

WF_absolute.thy

Wellorderings.thy

IMP/

Induct/

Binary_Trees.thy

InfDatatype.thy

Resid/

UNITY/

Distributor.thy

Monotonicity.thy

MultisetSum.thy

ex/

Commutation.thy

rISABELLE0c18df79b1c8

src/ZF/AC/AC15_WO6.thy

src/ZF/AC/AC16_WO4.thy

src/ZF/AC/AC16_lemmas.thy

src/ZF/AC/AC17_AC1.thy

src/ZF/AC/AC18_AC19.thy

src/ZF/AC/AC7_AC9.thy

src/ZF/AC/AC_Equiv.thy

src/ZF/AC/Cardinal_aux.thy

src/ZF/AC/DC.thy

src/ZF/AC/HH.thy

src/ZF/AC/Hartog.thy

src/ZF/AC/WO1_AC.thy

src/ZF/AC/WO1_WO7.thy

src/ZF/AC/WO2_AC16.thy

src/ZF/AC/WO6_WO1.thy

src/ZF/Arith.thy

src/ZF/ArithSimp.thy

src/ZF/Bin.thy

src/ZF/Cardinal.thy

src/ZF/CardinalArith.thy

src/ZF/Coind/ECR.thy

src/ZF/Coind/Static.thy

src/ZF/Constructible/AC_in_L.thy

src/ZF/Constructible/DPow_absolute.thy

src/ZF/Constructible/Datatype_absolute.thy

src/ZF/Constructible/Formula.thy

src/ZF/Constructible/Internalize.thy

src/ZF/Constructible/L_axioms.thy

src/ZF/Constructible/Rank.thy

src/ZF/Constructible/Rank_Separation.thy

src/ZF/Constructible/Rec_Separation.thy

src/ZF/Constructible/Reflection.thy

src/ZF/Constructible/Relative.thy

src/ZF/Constructible/Satisfies_absolute.thy

src/ZF/Constructible/Separation.thy

src/ZF/Constructible/WF_absolute.thy

src/ZF/Constructible/WFrec.thy

src/ZF/Constructible/Wellorderings.thy

src/ZF/Epsilon.thy

src/ZF/EquivClass.thy

src/ZF/Finite.thy

src/ZF/Fixedpt.thy

src/ZF/IMP/Denotation.thy

src/ZF/Induct/Binary_Trees.thy

src/ZF/Induct/Comb.thy

src/ZF/Induct/FoldSet.thy

src/ZF/Induct/ListN.thy

src/ZF/Induct/Multiset.thy

src/ZF/Induct/Mutil.thy

src/ZF/Induct/PropLog.thy

src/ZF/Induct/Term.thy

src/ZF/InfDatatype.thy

src/ZF/Int.thy

src/ZF/IntDiv.thy

src/ZF/List.thy

src/ZF/Nat.thy

src/ZF/OrdQuant.thy

src/ZF/Order.thy

src/ZF/OrderArith.thy

src/ZF/OrderType.thy

src/ZF/Ordinal.thy

src/ZF/Perm.thy

src/ZF/QPair.thy

src/ZF/QUniv.thy

src/ZF/Resid/Confluence.thy

src/ZF/Resid/Reduction.thy

src/ZF/Resid/Residuals.thy

src/ZF/Sum.thy

src/ZF/Trancl.thy

src/ZF/UNITY/AllocBase.thy

src/ZF/UNITY/AllocImpl.thy

src/ZF/UNITY/ClientImpl.thy

src/ZF/UNITY/Comp.thy

src/ZF/UNITY/Constrains.thy

src/ZF/UNITY/Distributor.thy

src/ZF/UNITY/Follows.thy

src/ZF/UNITY/GenPrefix.thy

src/ZF/UNITY/Guar.thy

src/ZF/UNITY/Increasing.thy

src/ZF/UNITY/Merge.thy

src/ZF/UNITY/Monotonicity.thy

src/ZF/UNITY/MultisetSum.thy

src/ZF/UNITY/Mutex.thy

src/ZF/UNITY/State.thy

src/ZF/UNITY/SubstAx.thy

src/ZF/UNITY/UNITY.thy

src/ZF/UNITY/Union.thy

src/ZF/UNITY/WFair.thy

src/ZF/Univ.thy

src/ZF/ZF_Base.thy

src/ZF/Zorn.thy

src/ZF/equalities.thy

src/ZF/ex/CoUnit.thy

src/ZF/ex/Commutation.thy

src/ZF/ex/Group.thy

src/ZF/ex/LList.thy

src/ZF/ex/Limit.thy

src/ZF/ex/NatSum.thy

src/ZF/ex/Primes.thy

src/ZF/ex/Ramsey.thy

src/ZF/ex/Ring.thy

src/ZF/ex/misc.thy

src/ZF/func.thy

src/ZF/pair.thy

src/ZF/upair.thy