Changes

Summary

added a couple of structured proofs
More obsolete "unfold" calls
getting rid of apply (unfold ...)
More syntactic cleanup. LaTeX markup working
more modernisation of syntax
Removal of obsolete ASCII syntax
clarified options;

Changeset 76218:728f38b016c0 by paulson _lp15@cam.ac.uk_: added a couple of structured proofs
The file was modified	`src/ZF/Constructible/Normal.thy` (diff)
Changeset 76217:8655344f1cf6 by paulson _lp15@cam.ac.uk_: More obsolete "unfold" calls
The file was modified	`src/ZF/AC/AC15_WO6.thy` (diff)
The file was modified	`src/ZF/AC/AC16_WO4.thy` (diff)
The file was modified	`src/ZF/AC/AC16_lemmas.thy` (diff)
The file was modified	`src/ZF/AC/AC17_AC1.thy` (diff)
The file was modified	`src/ZF/AC/AC7_AC9.thy` (diff)
The file was modified	`src/ZF/AC/DC.thy` (diff)
The file was modified	`src/ZF/AC/HH.thy` (diff)
The file was modified	`src/ZF/AC/WO1_AC.thy` (diff)
The file was modified	`src/ZF/AC/WO1_WO7.thy` (diff)
The file was modified	`src/ZF/AC/WO2_AC16.thy` (diff)
The file was modified	`src/ZF/AC/WO6_WO1.thy` (diff)
The file was modified	`src/ZF/Bin.thy` (diff)
The file was modified	`src/ZF/Cardinal.thy` (diff)
The file was modified	`src/ZF/CardinalArith.thy` (diff)
The file was modified	`src/ZF/Coind/ECR.thy` (diff)
The file was modified	`src/ZF/Coind/Map.thy` (diff)
The file was modified	`src/ZF/Coind/Values.thy` (diff)
The file was modified	`src/ZF/Constructible/L_axioms.thy` (diff)
The file was modified	`src/ZF/Constructible/Rank.thy` (diff)
The file was modified	`src/ZF/Constructible/Reflection.thy` (diff)
The file was modified	`src/ZF/Constructible/Relative.thy` (diff)
The file was modified	`src/ZF/Constructible/Satisfies_absolute.thy` (diff)
The file was modified	`src/ZF/Epsilon.thy` (diff)
The file was modified	`src/ZF/EquivClass.thy` (diff)
The file was modified	`src/ZF/Finite.thy` (diff)
The file was modified	`src/ZF/Induct/Binary_Trees.thy` (diff)
The file was modified	`src/ZF/Induct/Datatypes.thy` (diff)
The file was modified	`src/ZF/Induct/ListN.thy` (diff)
The file was modified	`src/ZF/Induct/Multiset.thy` (diff)
The file was modified	`src/ZF/Induct/Ntree.thy` (diff)
The file was modified	`src/ZF/Induct/PropLog.thy` (diff)
The file was modified	`src/ZF/Induct/Rmap.thy` (diff)
The file was modified	`src/ZF/Induct/Term.thy` (diff)
The file was modified	`src/ZF/Induct/Tree_Forest.thy` (diff)
The file was modified	`src/ZF/List.thy` (diff)
The file was modified	`src/ZF/Order.thy` (diff)
The file was modified	`src/ZF/OrderArith.thy` (diff)
The file was modified	`src/ZF/OrderType.thy` (diff)
The file was modified	`src/ZF/Perm.thy` (diff)
The file was modified	`src/ZF/QUniv.thy` (diff)
The file was modified	`src/ZF/Resid/Confluence.thy` (diff)
The file was modified	`src/ZF/Trancl.thy` (diff)
The file was modified	`src/ZF/UNITY/AllocBase.thy` (diff)
The file was modified	`src/ZF/UNITY/ClientImpl.thy` (diff)
The file was modified	`src/ZF/UNITY/Comp.thy` (diff)
The file was modified	`src/ZF/UNITY/Constrains.thy` (diff)
The file was modified	`src/ZF/UNITY/FP.thy` (diff)
The file was modified	`src/ZF/UNITY/Follows.thy` (diff)
The file was modified	`src/ZF/UNITY/GenPrefix.thy` (diff)
The file was modified	`src/ZF/UNITY/Increasing.thy` (diff)
The file was modified	`src/ZF/UNITY/Monotonicity.thy` (diff)
The file was modified	`src/ZF/UNITY/UNITY.thy` (diff)
The file was modified	`src/ZF/UNITY/Union.thy` (diff)
The file was modified	`src/ZF/UNITY/WFair.thy` (diff)
The file was modified	`src/ZF/WF.thy` (diff)
The file was modified	`src/ZF/ZF_Base.thy` (diff)
The file was modified	`src/ZF/Zorn.thy` (diff)
The file was modified	`src/ZF/ex/CoUnit.thy` (diff)
The file was modified	`src/ZF/ex/Commutation.thy` (diff)
The file was modified	`src/ZF/ex/Group.thy` (diff)
The file was modified	`src/ZF/ex/LList.thy` (diff)
The file was modified	`src/ZF/ex/Ramsey.thy` (diff)
The file was modified	`src/ZF/func.thy` (diff)
Changeset 76216:9fc34f76b4e8 by paulson _lp15@cam.ac.uk_: getting rid of apply (unfold ...)
The file was modified	`src/ZF/AC/AC15_WO6.thy` (diff)
The file was modified	`src/ZF/AC/AC16_WO4.thy` (diff)
The file was modified	`src/ZF/AC/AC16_lemmas.thy` (diff)
The file was modified	`src/ZF/AC/AC17_AC1.thy` (diff)
The file was modified	`src/ZF/AC/AC18_AC19.thy` (diff)
The file was modified	`src/ZF/AC/AC7_AC9.thy` (diff)
The file was modified	`src/ZF/AC/AC_Equiv.thy` (diff)
The file was modified	`src/ZF/AC/Cardinal_aux.thy` (diff)
The file was modified	`src/ZF/AC/DC.thy` (diff)
The file was modified	`src/ZF/AC/HH.thy` (diff)
The file was modified	`src/ZF/AC/Hartog.thy` (diff)
The file was modified	`src/ZF/AC/WO1_AC.thy` (diff)
The file was modified	`src/ZF/AC/WO1_WO7.thy` (diff)
The file was modified	`src/ZF/AC/WO2_AC16.thy` (diff)
The file was modified	`src/ZF/AC/WO6_WO1.thy` (diff)
The file was modified	`src/ZF/Arith.thy` (diff)
The file was modified	`src/ZF/ArithSimp.thy` (diff)
The file was modified	`src/ZF/Bin.thy` (diff)
The file was modified	`src/ZF/Cardinal.thy` (diff)
The file was modified	`src/ZF/CardinalArith.thy` (diff)
The file was modified	`src/ZF/Coind/ECR.thy` (diff)
The file was modified	`src/ZF/Coind/Map.thy` (diff)
The file was modified	`src/ZF/Coind/Values.thy` (diff)
The file was modified	`src/ZF/Constructible/AC_in_L.thy` (diff)
The file was modified	`src/ZF/Constructible/DPow_absolute.thy` (diff)
The file was modified	`src/ZF/Constructible/Formula.thy` (diff)
The file was modified	`src/ZF/Constructible/L_axioms.thy` (diff)
The file was modified	`src/ZF/Constructible/Normal.thy` (diff)
The file was modified	`src/ZF/Constructible/Satisfies_absolute.thy` (diff)
The file was modified	`src/ZF/Constructible/Wellorderings.thy` (diff)
The file was modified	`src/ZF/Epsilon.thy` (diff)
The file was modified	`src/ZF/EquivClass.thy` (diff)
The file was modified	`src/ZF/Fixedpt.thy` (diff)
The file was modified	`src/ZF/IMP/Equiv.thy` (diff)
The file was modified	`src/ZF/Induct/Comb.thy` (diff)
The file was modified	`src/ZF/Induct/FoldSet.thy` (diff)
The file was modified	`src/ZF/Induct/Multiset.thy` (diff)
The file was modified	`src/ZF/Induct/Primrec.thy` (diff)
The file was modified	`src/ZF/Induct/PropLog.thy` (diff)
The file was modified	`src/ZF/Induct/Rmap.thy` (diff)
The file was modified	`src/ZF/Induct/Term.thy` (diff)
The file was modified	`src/ZF/Induct/Tree_Forest.thy` (diff)
The file was modified	`src/ZF/IntDiv.thy` (diff)
The file was modified	`src/ZF/List.thy` (diff)
The file was modified	`src/ZF/Nat.thy` (diff)
The file was modified	`src/ZF/Order.thy` (diff)
The file was modified	`src/ZF/OrderArith.thy` (diff)
The file was modified	`src/ZF/OrderType.thy` (diff)
The file was modified	`src/ZF/Ordinal.thy` (diff)
The file was modified	`src/ZF/Perm.thy` (diff)
The file was modified	`src/ZF/QUniv.thy` (diff)
The file was modified	`src/ZF/Resid/Confluence.thy` (diff)
The file was modified	`src/ZF/Resid/Residuals.thy` (diff)
The file was modified	`src/ZF/Sum.thy` (diff)
The file was modified	`src/ZF/Trancl.thy` (diff)
The file was modified	`src/ZF/UNITY/AllocBase.thy` (diff)
The file was modified	`src/ZF/UNITY/AllocImpl.thy` (diff)
The file was modified	`src/ZF/UNITY/ClientImpl.thy` (diff)
The file was modified	`src/ZF/UNITY/Comp.thy` (diff)
The file was modified	`src/ZF/UNITY/Constrains.thy` (diff)
The file was modified	`src/ZF/UNITY/Distributor.thy` (diff)
The file was modified	`src/ZF/UNITY/FP.thy` (diff)
The file was modified	`src/ZF/UNITY/Follows.thy` (diff)
The file was modified	`src/ZF/UNITY/GenPrefix.thy` (diff)
The file was modified	`src/ZF/UNITY/Guar.thy` (diff)
The file was modified	`src/ZF/UNITY/Increasing.thy` (diff)
The file was modified	`src/ZF/UNITY/Merge.thy` (diff)
The file was modified	`src/ZF/UNITY/Monotonicity.thy` (diff)
The file was modified	`src/ZF/UNITY/Mutex.thy` (diff)
The file was modified	`src/ZF/UNITY/SubstAx.thy` (diff)
The file was modified	`src/ZF/UNITY/UNITY.thy` (diff)
The file was modified	`src/ZF/UNITY/Union.thy` (diff)
The file was modified	`src/ZF/UNITY/WFair.thy` (diff)
The file was modified	`src/ZF/Univ.thy` (diff)
The file was modified	`src/ZF/WF.thy` (diff)
The file was modified	`src/ZF/ZF_Base.thy` (diff)
The file was modified	`src/ZF/Zorn.thy` (diff)
The file was modified	`src/ZF/equalities.thy` (diff)
The file was modified	`src/ZF/ex/Commutation.thy` (diff)
The file was modified	`src/ZF/ex/Limit.thy` (diff)
The file was modified	`src/ZF/ex/Ramsey.thy` (diff)
The file was modified	`src/ZF/func.thy` (diff)
The file was modified	`src/ZF/pair.thy` (diff)
The file was modified	`src/ZF/upair.thy` (diff)
Changeset 76215:a642599ffdea by paulson _lp15@cam.ac.uk_: More syntactic cleanup. LaTeX markup working
The file was modified	`src/ZF/AC.thy` (diff)
The file was modified	`src/ZF/AC/AC15_WO6.thy` (diff)
The file was modified	`src/ZF/AC/AC16_WO4.thy` (diff)
The file was modified	`src/ZF/AC/AC16_lemmas.thy` (diff)
The file was modified	`src/ZF/AC/AC18_AC19.thy` (diff)
The file was modified	`src/ZF/AC/AC7_AC9.thy` (diff)
The file was modified	`src/ZF/AC/AC_Equiv.thy` (diff)
The file was modified	`src/ZF/AC/Cardinal_aux.thy` (diff)
The file was modified	`src/ZF/AC/DC.thy` (diff)
The file was modified	`src/ZF/AC/HH.thy` (diff)
The file was modified	`src/ZF/AC/Hartog.thy` (diff)
The file was modified	`src/ZF/AC/WO2_AC16.thy` (diff)
The file was modified	`src/ZF/AC/WO6_WO1.thy` (diff)
The file was modified	`src/ZF/Arith.thy` (diff)
The file was modified	`src/ZF/Bin.thy` (diff)
The file was modified	`src/ZF/Bool.thy` (diff)
The file was modified	`src/ZF/Cardinal.thy` (diff)
The file was modified	`src/ZF/CardinalArith.thy` (diff)
The file was modified	`src/ZF/Cardinal_AC.thy` (diff)
The file was modified	`src/ZF/Coind/ECR.thy` (diff)
The file was modified	`src/ZF/Coind/Language.thy` (diff)
The file was modified	`src/ZF/Coind/Map.thy` (diff)
The file was modified	`src/ZF/Coind/Static.thy` (diff)
The file was modified	`src/ZF/Coind/Types.thy` (diff)
The file was modified	`src/ZF/Coind/Values.thy` (diff)
The file was modified	`src/ZF/Constructible/AC_in_L.thy` (diff)
The file was modified	`src/ZF/Constructible/DPow_absolute.thy` (diff)
The file was modified	`src/ZF/Constructible/Datatype_absolute.thy` (diff)
The file was modified	`src/ZF/Constructible/Formula.thy` (diff)
The file was modified	`src/ZF/Constructible/Internalize.thy` (diff)
The file was modified	`src/ZF/Constructible/L_axioms.thy` (diff)
The file was modified	`src/ZF/Constructible/Normal.thy` (diff)
The file was modified	`src/ZF/Constructible/Rank.thy` (diff)
The file was modified	`src/ZF/Constructible/Rank_Separation.thy` (diff)
The file was modified	`src/ZF/Constructible/Rec_Separation.thy` (diff)
The file was modified	`src/ZF/Constructible/Reflection.thy` (diff)
The file was modified	`src/ZF/Constructible/Relative.thy` (diff)
The file was modified	`src/ZF/Constructible/Satisfies_absolute.thy` (diff)
The file was modified	`src/ZF/Constructible/WF_absolute.thy` (diff)
The file was modified	`src/ZF/Constructible/WFrec.thy` (diff)
The file was modified	`src/ZF/Constructible/Wellorderings.thy` (diff)
The file was modified	`src/ZF/Epsilon.thy` (diff)
The file was modified	`src/ZF/EquivClass.thy` (diff)
The file was modified	`src/ZF/Finite.thy` (diff)
The file was modified	`src/ZF/Fixedpt.thy` (diff)
The file was modified	`src/ZF/IMP/Com.thy` (diff)
The file was modified	`src/ZF/IMP/Denotation.thy` (diff)
The file was modified	`src/ZF/IMP/Equiv.thy` (diff)
The file was modified	`src/ZF/Induct/Acc.thy` (diff)
The file was modified	`src/ZF/Induct/Binary_Trees.thy` (diff)
The file was modified	`src/ZF/Induct/Brouwer.thy` (diff)
The file was modified	`src/ZF/Induct/Comb.thy` (diff)
The file was modified	`src/ZF/Induct/Datatypes.thy` (diff)
The file was modified	`src/ZF/Induct/FoldSet.thy` (diff)
The file was modified	`src/ZF/Induct/ListN.thy` (diff)
The file was modified	`src/ZF/Induct/Multiset.thy` (diff)
The file was modified	`src/ZF/Induct/Mutil.thy` (diff)
The file was modified	`src/ZF/Induct/Ntree.thy` (diff)
The file was modified	`src/ZF/Induct/Primrec.thy` (diff)
The file was modified	`src/ZF/Induct/PropLog.thy` (diff)
The file was modified	`src/ZF/Induct/Rmap.thy` (diff)
The file was modified	`src/ZF/Induct/Term.thy` (diff)
The file was modified	`src/ZF/Induct/Tree_Forest.thy` (diff)
The file was modified	`src/ZF/Int.thy` (diff)
The file was modified	`src/ZF/IntDiv.thy` (diff)
The file was modified	`src/ZF/List.thy` (diff)
The file was modified	`src/ZF/Nat.thy` (diff)
The file was modified	`src/ZF/OrdQuant.thy` (diff)
The file was modified	`src/ZF/Order.thy` (diff)
The file was modified	`src/ZF/OrderArith.thy` (diff)
The file was modified	`src/ZF/OrderType.thy` (diff)
The file was modified	`src/ZF/Ordinal.thy` (diff)
The file was modified	`src/ZF/Perm.thy` (diff)
The file was modified	`src/ZF/QPair.thy` (diff)
The file was modified	`src/ZF/QUniv.thy` (diff)
The file was modified	`src/ZF/Resid/Confluence.thy` (diff)
The file was modified	`src/ZF/Resid/Redex.thy` (diff)
The file was modified	`src/ZF/Resid/Reduction.thy` (diff)
The file was modified	`src/ZF/Resid/Residuals.thy` (diff)
The file was modified	`src/ZF/Resid/Substitution.thy` (diff)
The file was modified	`src/ZF/Sum.thy` (diff)
The file was modified	`src/ZF/Trancl.thy` (diff)
The file was modified	`src/ZF/UNITY/AllocBase.thy` (diff)
The file was modified	`src/ZF/UNITY/AllocImpl.thy` (diff)
The file was modified	`src/ZF/UNITY/ClientImpl.thy` (diff)
The file was modified	`src/ZF/UNITY/Comp.thy` (diff)
The file was modified	`src/ZF/UNITY/Constrains.thy` (diff)
The file was modified	`src/ZF/UNITY/Distributor.thy` (diff)
The file was modified	`src/ZF/UNITY/FP.thy` (diff)
The file was modified	`src/ZF/UNITY/Follows.thy` (diff)
The file was modified	`src/ZF/UNITY/GenPrefix.thy` (diff)
The file was modified	`src/ZF/UNITY/Guar.thy` (diff)
The file was modified	`src/ZF/UNITY/Increasing.thy` (diff)
The file was modified	`src/ZF/UNITY/Merge.thy` (diff)
The file was modified	`src/ZF/UNITY/Monotonicity.thy` (diff)
The file was modified	`src/ZF/UNITY/MultisetSum.thy` (diff)
The file was modified	`src/ZF/UNITY/Mutex.thy` (diff)
The file was modified	`src/ZF/UNITY/State.thy` (diff)
The file was modified	`src/ZF/UNITY/SubstAx.thy` (diff)
The file was modified	`src/ZF/UNITY/UNITY.thy` (diff)
The file was modified	`src/ZF/UNITY/Union.thy` (diff)
The file was modified	`src/ZF/UNITY/WFair.thy` (diff)
The file was modified	`src/ZF/Univ.thy` (diff)
The file was modified	`src/ZF/WF.thy` (diff)
The file was modified	`src/ZF/ZF.thy` (diff)
The file was modified	`src/ZF/ZF_Base.thy` (diff)
The file was modified	`src/ZF/Zorn.thy` (diff)
The file was modified	`src/ZF/equalities.thy` (diff)
The file was modified	`src/ZF/ex/CoUnit.thy` (diff)
The file was modified	`src/ZF/ex/Commutation.thy` (diff)
The file was modified	`src/ZF/ex/Group.thy` (diff)
The file was modified	`src/ZF/ex/LList.thy` (diff)
The file was modified	`src/ZF/ex/Limit.thy` (diff)
The file was modified	`src/ZF/ex/NatSum.thy` (diff)
The file was modified	`src/ZF/ex/Primes.thy` (diff)
The file was modified	`src/ZF/ex/Ramsey.thy` (diff)
The file was modified	`src/ZF/ex/Ring.thy` (diff)
The file was modified	`src/ZF/ex/misc.thy` (diff)
The file was modified	`src/ZF/func.thy` (diff)
The file was modified	`src/ZF/pair.thy` (diff)
The file was modified	`src/ZF/upair.thy` (diff)
Changeset 76214:0c18df79b1c8 by paulson _lp15@cam.ac.uk_: more modernisation of syntax
The file was modified	`src/ZF/AC/AC15_WO6.thy` (diff)
The file was modified	`src/ZF/AC/AC16_WO4.thy` (diff)
The file was modified	`src/ZF/AC/AC16_lemmas.thy` (diff)
The file was modified	`src/ZF/AC/AC17_AC1.thy` (diff)
The file was modified	`src/ZF/AC/AC18_AC19.thy` (diff)
The file was modified	`src/ZF/AC/AC7_AC9.thy` (diff)
The file was modified	`src/ZF/AC/AC_Equiv.thy` (diff)
The file was modified	`src/ZF/AC/Cardinal_aux.thy` (diff)
The file was modified	`src/ZF/AC/DC.thy` (diff)
The file was modified	`src/ZF/AC/HH.thy` (diff)
The file was modified	`src/ZF/AC/Hartog.thy` (diff)
The file was modified	`src/ZF/AC/WO1_AC.thy` (diff)
The file was modified	`src/ZF/AC/WO1_WO7.thy` (diff)
The file was modified	`src/ZF/AC/WO2_AC16.thy` (diff)
The file was modified	`src/ZF/AC/WO6_WO1.thy` (diff)
The file was modified	`src/ZF/Arith.thy` (diff)
The file was modified	`src/ZF/ArithSimp.thy` (diff)
The file was modified	`src/ZF/Bin.thy` (diff)
The file was modified	`src/ZF/Cardinal.thy` (diff)
The file was modified	`src/ZF/CardinalArith.thy` (diff)
The file was modified	`src/ZF/Coind/ECR.thy` (diff)
The file was modified	`src/ZF/Coind/Static.thy` (diff)
The file was modified	`src/ZF/Constructible/AC_in_L.thy` (diff)
The file was modified	`src/ZF/Constructible/DPow_absolute.thy` (diff)
The file was modified	`src/ZF/Constructible/Datatype_absolute.thy` (diff)
The file was modified	`src/ZF/Constructible/Formula.thy` (diff)
The file was modified	`src/ZF/Constructible/Internalize.thy` (diff)
The file was modified	`src/ZF/Constructible/L_axioms.thy` (diff)
The file was modified	`src/ZF/Constructible/Rank.thy` (diff)
The file was modified	`src/ZF/Constructible/Rank_Separation.thy` (diff)
The file was modified	`src/ZF/Constructible/Rec_Separation.thy` (diff)
The file was modified	`src/ZF/Constructible/Reflection.thy` (diff)
The file was modified	`src/ZF/Constructible/Relative.thy` (diff)
The file was modified	`src/ZF/Constructible/Satisfies_absolute.thy` (diff)
The file was modified	`src/ZF/Constructible/Separation.thy` (diff)
The file was modified	`src/ZF/Constructible/WF_absolute.thy` (diff)
The file was modified	`src/ZF/Constructible/WFrec.thy` (diff)
The file was modified	`src/ZF/Constructible/Wellorderings.thy` (diff)
The file was modified	`src/ZF/Epsilon.thy` (diff)
The file was modified	`src/ZF/EquivClass.thy` (diff)
The file was modified	`src/ZF/Finite.thy` (diff)
The file was modified	`src/ZF/Fixedpt.thy` (diff)
The file was modified	`src/ZF/IMP/Denotation.thy` (diff)
The file was modified	`src/ZF/Induct/Binary_Trees.thy` (diff)
The file was modified	`src/ZF/Induct/Comb.thy` (diff)
The file was modified	`src/ZF/Induct/FoldSet.thy` (diff)
The file was modified	`src/ZF/Induct/ListN.thy` (diff)
The file was modified	`src/ZF/Induct/Multiset.thy` (diff)
The file was modified	`src/ZF/Induct/Mutil.thy` (diff)
The file was modified	`src/ZF/Induct/PropLog.thy` (diff)
The file was modified	`src/ZF/Induct/Term.thy` (diff)
The file was modified	`src/ZF/InfDatatype.thy` (diff)
The file was modified	`src/ZF/Int.thy` (diff)
The file was modified	`src/ZF/IntDiv.thy` (diff)
The file was modified	`src/ZF/List.thy` (diff)
The file was modified	`src/ZF/Nat.thy` (diff)
The file was modified	`src/ZF/OrdQuant.thy` (diff)
The file was modified	`src/ZF/Order.thy` (diff)
The file was modified	`src/ZF/OrderArith.thy` (diff)
The file was modified	`src/ZF/OrderType.thy` (diff)
The file was modified	`src/ZF/Ordinal.thy` (diff)
The file was modified	`src/ZF/Perm.thy` (diff)
The file was modified	`src/ZF/QPair.thy` (diff)
The file was modified	`src/ZF/QUniv.thy` (diff)
The file was modified	`src/ZF/Resid/Confluence.thy` (diff)
The file was modified	`src/ZF/Resid/Reduction.thy` (diff)
The file was modified	`src/ZF/Resid/Residuals.thy` (diff)
The file was modified	`src/ZF/Sum.thy` (diff)
The file was modified	`src/ZF/Trancl.thy` (diff)
The file was modified	`src/ZF/UNITY/AllocBase.thy` (diff)
The file was modified	`src/ZF/UNITY/AllocImpl.thy` (diff)
The file was modified	`src/ZF/UNITY/ClientImpl.thy` (diff)
The file was modified	`src/ZF/UNITY/Comp.thy` (diff)
The file was modified	`src/ZF/UNITY/Constrains.thy` (diff)
The file was modified	`src/ZF/UNITY/Distributor.thy` (diff)
The file was modified	`src/ZF/UNITY/Follows.thy` (diff)
The file was modified	`src/ZF/UNITY/GenPrefix.thy` (diff)
The file was modified	`src/ZF/UNITY/Guar.thy` (diff)
The file was modified	`src/ZF/UNITY/Increasing.thy` (diff)
The file was modified	`src/ZF/UNITY/Merge.thy` (diff)
The file was modified	`src/ZF/UNITY/Monotonicity.thy` (diff)
The file was modified	`src/ZF/UNITY/MultisetSum.thy` (diff)
The file was modified	`src/ZF/UNITY/Mutex.thy` (diff)
The file was modified	`src/ZF/UNITY/State.thy` (diff)
The file was modified	`src/ZF/UNITY/SubstAx.thy` (diff)
The file was modified	`src/ZF/UNITY/UNITY.thy` (diff)
The file was modified	`src/ZF/UNITY/Union.thy` (diff)
The file was modified	`src/ZF/UNITY/WFair.thy` (diff)
The file was modified	`src/ZF/Univ.thy` (diff)
The file was modified	`src/ZF/ZF_Base.thy` (diff)
The file was modified	`src/ZF/Zorn.thy` (diff)
The file was modified	`src/ZF/equalities.thy` (diff)
The file was modified	`src/ZF/ex/CoUnit.thy` (diff)
The file was modified	`src/ZF/ex/Commutation.thy` (diff)
The file was modified	`src/ZF/ex/Group.thy` (diff)
The file was modified	`src/ZF/ex/LList.thy` (diff)
The file was modified	`src/ZF/ex/Limit.thy` (diff)
The file was modified	`src/ZF/ex/NatSum.thy` (diff)
The file was modified	`src/ZF/ex/Primes.thy` (diff)
The file was modified	`src/ZF/ex/Ramsey.thy` (diff)
The file was modified	`src/ZF/ex/Ring.thy` (diff)
The file was modified	`src/ZF/ex/misc.thy` (diff)
The file was modified	`src/ZF/func.thy` (diff)
The file was modified	`src/ZF/pair.thy` (diff)
The file was modified	`src/ZF/upair.thy` (diff)
Changeset 76213:e44d86131648 by paulson _lp15@cam.ac.uk_: Removal of obsolete ASCII syntax
The file was modified	`src/ZF/AC.thy` (diff)
The file was modified	`src/ZF/AC/AC15_WO6.thy` (diff)
The file was modified	`src/ZF/AC/AC16_WO4.thy` (diff)
The file was modified	`src/ZF/AC/AC16_lemmas.thy` (diff)
The file was modified	`src/ZF/AC/AC17_AC1.thy` (diff)
The file was modified	`src/ZF/AC/AC18_AC19.thy` (diff)
The file was modified	`src/ZF/AC/AC7_AC9.thy` (diff)
The file was modified	`src/ZF/AC/AC_Equiv.thy` (diff)
The file was modified	`src/ZF/AC/Cardinal_aux.thy` (diff)
The file was modified	`src/ZF/AC/DC.thy` (diff)
The file was modified	`src/ZF/AC/HH.thy` (diff)
The file was modified	`src/ZF/AC/Hartog.thy` (diff)
The file was modified	`src/ZF/AC/WO1_AC.thy` (diff)
The file was modified	`src/ZF/AC/WO1_WO7.thy` (diff)
The file was modified	`src/ZF/AC/WO2_AC16.thy` (diff)
The file was modified	`src/ZF/AC/WO6_WO1.thy` (diff)
The file was modified	`src/ZF/Arith.thy` (diff)
The file was modified	`src/ZF/ArithSimp.thy` (diff)
The file was modified	`src/ZF/Bin.thy` (diff)
The file was modified	`src/ZF/Bool.thy` (diff)
The file was modified	`src/ZF/Cardinal.thy` (diff)
The file was modified	`src/ZF/CardinalArith.thy` (diff)
The file was modified	`src/ZF/Cardinal_AC.thy` (diff)
The file was modified	`src/ZF/Coind/Dynamic.thy` (diff)
The file was modified	`src/ZF/Coind/ECR.thy` (diff)
The file was modified	`src/ZF/Coind/Language.thy` (diff)
The file was modified	`src/ZF/Coind/Map.thy` (diff)
The file was modified	`src/ZF/Coind/Static.thy` (diff)
The file was modified	`src/ZF/Coind/Types.thy` (diff)
The file was modified	`src/ZF/Coind/Values.thy` (diff)
The file was modified	`src/ZF/Constructible/AC_in_L.thy` (diff)
The file was modified	`src/ZF/Constructible/DPow_absolute.thy` (diff)
The file was modified	`src/ZF/Constructible/Datatype_absolute.thy` (diff)
The file was modified	`src/ZF/Constructible/Formula.thy` (diff)
The file was modified	`src/ZF/Constructible/Internalize.thy` (diff)
The file was modified	`src/ZF/Constructible/L_axioms.thy` (diff)
The file was modified	`src/ZF/Constructible/MetaExists.thy` (diff)
The file was modified	`src/ZF/Constructible/Normal.thy` (diff)
The file was modified	`src/ZF/Constructible/Rank.thy` (diff)
The file was modified	`src/ZF/Constructible/Rank_Separation.thy` (diff)
The file was modified	`src/ZF/Constructible/Rec_Separation.thy` (diff)
The file was modified	`src/ZF/Constructible/Reflection.thy` (diff)
The file was modified	`src/ZF/Constructible/Relative.thy` (diff)
The file was modified	`src/ZF/Constructible/Satisfies_absolute.thy` (diff)
The file was modified	`src/ZF/Constructible/Separation.thy` (diff)
The file was modified	`src/ZF/Constructible/WF_absolute.thy` (diff)
The file was modified	`src/ZF/Constructible/WFrec.thy` (diff)
The file was modified	`src/ZF/Constructible/Wellorderings.thy` (diff)
The file was modified	`src/ZF/Epsilon.thy` (diff)
The file was modified	`src/ZF/EquivClass.thy` (diff)
The file was modified	`src/ZF/Finite.thy` (diff)
The file was modified	`src/ZF/Fixedpt.thy` (diff)
The file was modified	`src/ZF/IMP/Com.thy` (diff)
The file was modified	`src/ZF/IMP/Denotation.thy` (diff)
The file was modified	`src/ZF/IMP/Equiv.thy` (diff)
The file was modified	`src/ZF/Induct/Acc.thy` (diff)
The file was modified	`src/ZF/Induct/Binary_Trees.thy` (diff)
The file was modified	`src/ZF/Induct/Brouwer.thy` (diff)
The file was modified	`src/ZF/Induct/Comb.thy` (diff)
The file was modified	`src/ZF/Induct/Datatypes.thy` (diff)
The file was modified	`src/ZF/Induct/FoldSet.thy` (diff)
The file was modified	`src/ZF/Induct/ListN.thy` (diff)
The file was modified	`src/ZF/Induct/Multiset.thy` (diff)
The file was modified	`src/ZF/Induct/Mutil.thy` (diff)
The file was modified	`src/ZF/Induct/Ntree.thy` (diff)
The file was modified	`src/ZF/Induct/Primrec.thy` (diff)
The file was modified	`src/ZF/Induct/PropLog.thy` (diff)
The file was modified	`src/ZF/Induct/Rmap.thy` (diff)
The file was modified	`src/ZF/Induct/Term.thy` (diff)
The file was modified	`src/ZF/Induct/Tree_Forest.thy` (diff)
The file was modified	`src/ZF/Inductive.thy` (diff)
The file was modified	`src/ZF/InfDatatype.thy` (diff)
The file was modified	`src/ZF/Int.thy` (diff)
The file was modified	`src/ZF/IntDiv.thy` (diff)
The file was modified	`src/ZF/List.thy` (diff)
The file was modified	`src/ZF/Nat.thy` (diff)
The file was modified	`src/ZF/OrdQuant.thy` (diff)
The file was modified	`src/ZF/Order.thy` (diff)
The file was modified	`src/ZF/OrderArith.thy` (diff)
The file was modified	`src/ZF/OrderType.thy` (diff)
The file was modified	`src/ZF/Ordinal.thy` (diff)
The file was modified	`src/ZF/Perm.thy` (diff)
The file was modified	`src/ZF/QPair.thy` (diff)
The file was modified	`src/ZF/QUniv.thy` (diff)
The file was modified	`src/ZF/Resid/Confluence.thy` (diff)
The file was modified	`src/ZF/Resid/Redex.thy` (diff)
The file was modified	`src/ZF/Resid/Reduction.thy` (diff)
The file was modified	`src/ZF/Resid/Residuals.thy` (diff)
The file was modified	`src/ZF/Resid/Substitution.thy` (diff)
The file was modified	`src/ZF/Sum.thy` (diff)
The file was modified	`src/ZF/Trancl.thy` (diff)
The file was modified	`src/ZF/UNITY/AllocBase.thy` (diff)
The file was modified	`src/ZF/UNITY/AllocImpl.thy` (diff)
The file was modified	`src/ZF/UNITY/ClientImpl.thy` (diff)
The file was modified	`src/ZF/UNITY/Comp.thy` (diff)
The file was modified	`src/ZF/UNITY/Constrains.thy` (diff)
The file was modified	`src/ZF/UNITY/Distributor.thy` (diff)
The file was modified	`src/ZF/UNITY/FP.thy` (diff)
The file was modified	`src/ZF/UNITY/Follows.thy` (diff)
The file was modified	`src/ZF/UNITY/GenPrefix.thy` (diff)
The file was modified	`src/ZF/UNITY/Guar.thy` (diff)
The file was modified	`src/ZF/UNITY/Increasing.thy` (diff)
The file was modified	`src/ZF/UNITY/Merge.thy` (diff)
The file was modified	`src/ZF/UNITY/Monotonicity.thy` (diff)
The file was modified	`src/ZF/UNITY/MultisetSum.thy` (diff)
The file was modified	`src/ZF/UNITY/Mutex.thy` (diff)
The file was modified	`src/ZF/UNITY/State.thy` (diff)
The file was modified	`src/ZF/UNITY/SubstAx.thy` (diff)
The file was modified	`src/ZF/UNITY/UNITY.thy` (diff)
The file was modified	`src/ZF/UNITY/Union.thy` (diff)
The file was modified	`src/ZF/UNITY/WFair.thy` (diff)
The file was modified	`src/ZF/Univ.thy` (diff)
The file was modified	`src/ZF/WF.thy` (diff)
The file was modified	`src/ZF/ZF.thy` (diff)
The file was modified	`src/ZF/ZF_Base.thy` (diff)
The file was modified	`src/ZF/Zorn.thy` (diff)
The file was modified	`src/ZF/equalities.thy` (diff)
The file was modified	`src/ZF/ex/BinEx.thy` (diff)
The file was modified	`src/ZF/ex/CoUnit.thy` (diff)
The file was modified	`src/ZF/ex/Commutation.thy` (diff)
The file was modified	`src/ZF/ex/Group.thy` (diff)
The file was modified	`src/ZF/ex/LList.thy` (diff)
The file was modified	`src/ZF/ex/Limit.thy` (diff)
The file was modified	`src/ZF/ex/NatSum.thy` (diff)
The file was modified	`src/ZF/ex/Primes.thy` (diff)
The file was modified	`src/ZF/ex/Ramsey.thy` (diff)
The file was modified	`src/ZF/ex/Ring.thy` (diff)
The file was modified	`src/ZF/ex/misc.thy` (diff)
The file was modified	`src/ZF/func.thy` (diff)
The file was modified	`src/ZF/pair.thy` (diff)
The file was modified	`src/ZF/upair.thy` (diff)
Changeset 76212:f2094906e491 by wenzelm: clarified options;
The file was modified	`etc/options` (diff)
The file was modified	`src/Doc/ROOT` (diff)