Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

Summary

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