Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

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

Summary

  1. added a couple of structured proofs
  2. More obsolete "unfold" calls
  3. getting rid of apply (unfold ...)
  4. More syntactic cleanup. LaTeX markup working
  5. more modernisation of syntax
  6. Removal of obsolete ASCII syntax
  7. 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
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
Changeset 76212:f2094906e491 by wenzelm:
clarified options;
The file was modified etc/options
The file was modified src/Doc/ROOT

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

Summary

  1. merge from afp-2021-1
  2. regenerate site;
  3. afp site: minor stylistic improvements;
  4. web entry for Stalnaker_Logic
  5. new entry: Stalnaker Logic
  6. clarified options, following f2094906e491;
Changeset 13052:d81cfd823ae9 by fabian huch _huch@in.tum.de_:
merge from afp-2021-1
Changeset 13051:d34f0b952a04 by fabian huch _huch@in.tum.de_:
regenerate site;
The file was modified web/css/front.min.css
The file was modified web/entries/ADS_Functor.html
The file was modified web/entries/AI_Planning_Languages_Semantics.html
The file was modified web/entries/AODV.html
The file was modified web/entries/AVL-Trees.html
The file was modified web/entries/AWN.html
The file was modified web/entries/Abortable_Linearizable_Modules.html
The file was modified web/entries/Abs_Int_ITP2012.html
The file was modified web/entries/Abstract-Hoare-Logics.html
The file was modified web/entries/Abstract-Rewriting.html
The file was modified web/entries/Abstract_Completeness.html
The file was modified web/entries/Abstract_Soundness.html
The file was modified web/entries/Ackermanns_not_PR.html
The file was modified web/entries/Actuarial_Mathematics.html
The file was modified web/entries/Adaptive_State_Counting.html
The file was modified web/entries/Affine_Arithmetic.html
The file was modified web/entries/Aggregation_Algebras.html
The file was modified web/entries/Akra_Bazzi.html
The file was modified web/entries/Algebraic_Numbers.html
The file was modified web/entries/Algebraic_VCs.html
The file was modified web/entries/Allen_Calculus.html
The file was modified web/entries/Amicable_Numbers.html
The file was modified web/entries/Amortized_Complexity.html
The file was modified web/entries/AnselmGod.html
The file was modified web/entries/Applicative_Lifting.html
The file was modified web/entries/Approximation_Algorithms.html
The file was modified web/entries/Architectural_Design_Patterns.html
The file was modified web/entries/Aristotles_Assertoric_Syllogistic.html
The file was modified web/entries/Arith_Prog_Rel_Primes.html
The file was modified web/entries/ArrowImpossibilityGS.html
The file was modified web/entries/Attack_Trees.html
The file was modified web/entries/Auto2_HOL.html
The file was modified web/entries/Auto2_Imperative_HOL.html
The file was modified web/entries/AutoFocus-Stream.html
The file was modified web/entries/Automated_Stateful_Protocol_Verification.html
The file was modified web/entries/Automatic_Refinement.html
The file was modified web/entries/AxiomaticCategoryTheory.html
The file was modified web/entries/BDD.html
The file was modified web/entries/BD_Security_Compositional.html
The file was modified web/entries/BNF_CC.html
The file was modified web/entries/BNF_Operations.html
The file was modified web/entries/BTree.html
The file was modified web/entries/Banach_Steinhaus.html
The file was modified web/entries/Belief_Revision.html
The file was modified web/entries/Bell_Numbers_Spivey.html
The file was modified web/entries/BenOr_Kozen_Reif.html
The file was modified web/entries/Berlekamp_Zassenhaus.html
The file was modified web/entries/Bernoulli.html
The file was modified web/entries/Bertrands_Postulate.html
The file was modified web/entries/Bicategory.html
The file was modified web/entries/BinarySearchTree.html
The file was modified web/entries/Binding_Syntax_Theory.html
The file was modified web/entries/Binomial-Heaps.html
The file was modified web/entries/Binomial-Queues.html
The file was modified web/entries/BirdKMP.html
The file was modified web/entries/Blue_Eyes.html
The file was modified web/entries/Bondy.html
The file was modified web/entries/Boolean_Expression_Checkers.html
The file was modified web/entries/Boolos_Curious_Inference.html
The file was modified web/entries/Bounded_Deducibility_Security.html
The file was modified web/entries/Buchi_Complementation.html
The file was modified web/entries/Budan_Fourier.html
The file was modified web/entries/Buffons_Needle.html
The file was modified web/entries/Buildings.html
The file was modified web/entries/BytecodeLogicJmlTypes.html
The file was modified web/entries/C2KA_DistributedSystems.html
The file was modified web/entries/CAVA_Automata.html
The file was modified web/entries/CAVA_LTL_Modelchecker.html
The file was modified web/entries/CCS.html
The file was modified web/entries/CISC-Kernel.html
The file was modified web/entries/CRDT.html
The file was modified web/entries/CRYSTALS-Kyber.html
The file was modified web/entries/CSP_RefTK.html
The file was modified web/entries/CYK.html
The file was modified web/entries/CZH_Elementary_Categories.html
The file was modified web/entries/CZH_Foundations.html
The file was modified web/entries/CZH_Universal_Constructions.html
The file was modified web/entries/CakeML.html
The file was modified web/entries/CakeML_Codegen.html
The file was modified web/entries/Call_Arity.html
The file was modified web/entries/Card_Equiv_Relations.html
The file was modified web/entries/Card_Multisets.html
The file was modified web/entries/Card_Number_Partitions.html
The file was modified web/entries/Card_Partitions.html
The file was modified web/entries/Cartan_FP.html
The file was modified web/entries/Case_Labeling.html
The file was modified web/entries/Catalan_Numbers.html
The file was modified web/entries/Category.html
The file was modified web/entries/Category2.html
The file was modified web/entries/Category3.html
The file was modified web/entries/Cauchy.html
The file was modified web/entries/Cayley_Hamilton.html
The file was modified web/entries/Certification_Monads.html
The file was modified web/entries/Chandy_Lamport.html
The file was modified web/entries/Chord_Segments.html
The file was modified web/entries/Circus.html
The file was modified web/entries/Clean.html
The file was modified web/entries/Clique_and_Monotone_Circuits.html
The file was modified web/entries/ClockSynchInst.html
The file was modified web/entries/Closest_Pair_Points.html
The file was modified web/entries/CoCon.html
The file was modified web/entries/CoSMeDis.html
The file was modified web/entries/CoSMed.html
The file was modified web/entries/CofGroups.html
The file was modified web/entries/Coinductive.html
The file was modified web/entries/Coinductive_Languages.html
The file was modified web/entries/Collections.html
The file was modified web/entries/Combinable_Wands.html
The file was modified web/entries/Combinatorics_Words.html
The file was modified web/entries/Combinatorics_Words_Graph_Lemma.html
The file was modified web/entries/Combinatorics_Words_Lyndon.html
The file was modified web/entries/Commuting_Hermitian.html
The file was modified web/entries/Comparison_Sort_Lower_Bound.html
The file was modified web/entries/Compiling-Exceptions-Correctly.html
The file was modified web/entries/Complete_Non_Orders.html
The file was modified web/entries/Completeness.html
The file was modified web/entries/Complex_Bounded_Operators.html
The file was modified web/entries/Complex_Geometry.html
The file was modified web/entries/Complx.html
The file was modified web/entries/ComponentDependencies.html
The file was modified web/entries/ConcurrentGC.html
The file was modified web/entries/ConcurrentIMP.html
The file was modified web/entries/Concurrent_Ref_Alg.html
The file was modified web/entries/Concurrent_Revisions.html
The file was modified web/entries/Conditional_Simplification.html
The file was modified web/entries/Conditional_Transfer_Rule.html
The file was modified web/entries/Consensus_Refined.html
The file was modified web/entries/Constructive_Cryptography.html
The file was modified web/entries/Constructive_Cryptography_CM.html
The file was modified web/entries/Constructor_Funs.html
The file was modified web/entries/Containers.html
The file was modified web/entries/CoreC++.html
The file was modified web/entries/Core_DOM.html
The file was modified web/entries/Core_SC_DOM.html
The file was modified web/entries/Correctness_Algebras.html
The file was modified web/entries/Cotangent_PFD_Formula.html
The file was modified web/entries/Count_Complex_Roots.html
The file was modified web/entries/CryptHOL.html
The file was modified web/entries/CryptoBasedCompositionalProperties.html
The file was modified web/entries/Cubic_Quartic_Equations.html
The file was modified web/entries/DFS_Framework.html
The file was modified web/entries/DOM_Components.html
The file was modified web/entries/DPRM_Theorem.html
The file was modified web/entries/DPT-SAT-Solver.html
The file was modified web/entries/DataRefinementIBP.html
The file was modified web/entries/Datatype_Order_Generator.html
The file was modified web/entries/Decl_Sem_Fun_PL.html
The file was modified web/entries/Decreasing-Diagrams-II.html
The file was modified web/entries/Decreasing-Diagrams.html
The file was modified web/entries/Dedekind_Real.html
The file was modified web/entries/Deep_Learning.html
The file was modified web/entries/Delta_System_Lemma.html
The file was modified web/entries/Density_Compiler.html
The file was modified web/entries/Dependent_SIFUM_Refinement.html
The file was modified web/entries/Dependent_SIFUM_Type_Systems.html
The file was modified web/entries/Depth-First-Search.html
The file was modified web/entries/Derangements.html
The file was modified web/entries/Deriving.html
The file was modified web/entries/Descartes_Sign_Rule.html
The file was modified web/entries/Design_Theory.html
The file was modified web/entries/Dict_Construction.html
The file was modified web/entries/Differential_Dynamic_Logic.html
The file was modified web/entries/Differential_Game_Logic.html
The file was modified web/entries/Digit_Expansions.html
The file was modified web/entries/Dijkstra_Shortest_Path.html
The file was modified web/entries/Diophantine_Eqns_Lin_Hom.html
The file was modified web/entries/Dirichlet_L.html
The file was modified web/entries/Dirichlet_Series.html
The file was modified web/entries/DiscretePricing.html
The file was modified web/entries/Discrete_Summation.html
The file was modified web/entries/DiskPaxos.html
The file was modified web/entries/Dominance_CHK.html
The file was modified web/entries/DynamicArchitectures.html
The file was modified web/entries/Dynamic_Tables.html
The file was modified web/entries/E_Transcendental.html
The file was modified web/entries/Echelon_Form.html
The file was modified web/entries/EdmondsKarp_Maxflow.html
The file was modified web/entries/Efficient-Mergesort.html
The file was modified web/entries/Elliptic_Curves_Group_Law.html
The file was modified web/entries/Encodability_Process_Calculi.html
The file was modified web/entries/Epistemic_Logic.html
The file was modified web/entries/Equivalence_Relation_Enumeration.html
The file was modified web/entries/Ergodic_Theory.html
The file was modified web/entries/Error_Function.html
The file was modified web/entries/Euler_MacLaurin.html
The file was modified web/entries/Euler_Partition.html
The file was modified web/entries/Eval_FO.html
The file was modified web/entries/Extended_Finite_State_Machine_Inference.html
The file was modified web/entries/Extended_Finite_State_Machines.html
The file was modified web/entries/FFT.html
The file was modified web/entries/FLP.html
The file was modified web/entries/FOL-Fitting.html
The file was modified web/entries/FOL_Axiomatic.html
The file was modified web/entries/FOL_Harrison.html
The file was modified web/entries/FOL_Seq_Calc1.html
The file was modified web/entries/FOL_Seq_Calc2.html
The file was modified web/entries/FOL_Seq_Calc3.html
The file was modified web/entries/FO_Theory_Rewriting.html
The file was modified web/entries/FSM_Tests.html
The file was modified web/entries/Factor_Algebraic_Polynomial.html
The file was modified web/entries/Factored_Transition_System_Bounding.html
The file was modified web/entries/Falling_Factorial_Sum.html
The file was modified web/entries/Farkas.html
The file was modified web/entries/FeatherweightJava.html
The file was modified web/entries/Featherweight_OCL.html
The file was modified web/entries/Fermat3_4.html
The file was modified web/entries/FileRefinement.html
The file was modified web/entries/FinFun.html
The file was modified web/entries/Finger-Trees.html
The file was modified web/entries/Finite-Map-Extras.html
The file was modified web/entries/Finite_Automata_HF.html
The file was modified web/entries/Finite_Fields.html
The file was modified web/entries/Finitely_Generated_Abelian_Groups.html
The file was modified web/entries/First_Order_Terms.html
The file was modified web/entries/First_Welfare_Theorem.html
The file was modified web/entries/Fishburn_Impossibility.html
The file was modified web/entries/Fisher_Yates.html
The file was modified web/entries/Fishers_Inequality.html
The file was modified web/entries/Flow_Networks.html
The file was modified web/entries/Floyd_Warshall.html
The file was modified web/entries/Flyspeck-Tame.html
The file was modified web/entries/FocusStreamsCaseStudies.html
The file was modified web/entries/Forcing.html
The file was modified web/entries/Formal_Puiseux_Series.html
The file was modified web/entries/Formal_SSA.html
The file was modified web/entries/Formula_Derivatives.html
The file was modified web/entries/Foundation_of_geometry.html
The file was modified web/entries/Fourier.html
The file was modified web/entries/Free-Boolean-Algebra.html
The file was modified web/entries/Free-Groups.html
The file was modified web/entries/Frequency_Moments.html
The file was modified web/entries/Fresh_Identifiers.html
The file was modified web/entries/FunWithFunctions.html
The file was modified web/entries/FunWithTilings.html
The file was modified web/entries/Functional-Automata.html
The file was modified web/entries/Functional_Ordered_Resolution_Prover.html
The file was modified web/entries/Furstenberg_Topology.html
The file was modified web/entries/GPU_Kernel_PL.html
The file was modified web/entries/Gabow_SCC.html
The file was modified web/entries/GaleStewart_Games.html
The file was modified web/entries/Gale_Shapley.html
The file was modified web/entries/Game_Based_Crypto.html
The file was modified web/entries/Gauss-Jordan-Elim-Fun.html
The file was modified web/entries/Gauss_Jordan.html
The file was modified web/entries/Gauss_Sums.html
The file was modified web/entries/Gaussian_Integers.html
The file was modified web/entries/GenClock.html
The file was modified web/entries/General-Triangle.html
The file was modified web/entries/Generalized_Counting_Sort.html
The file was modified web/entries/Generic_Deriving.html
The file was modified web/entries/Generic_Join.html
The file was modified web/entries/GewirthPGCProof.html
The file was modified web/entries/Girth_Chromatic.html
The file was modified web/entries/GoedelGod.html
The file was modified web/entries/Goedel_HFSet_Semantic.html
The file was modified web/entries/Goedel_HFSet_Semanticless.html
The file was modified web/entries/Goedel_Incompleteness.html
The file was modified web/entries/Goodstein_Lambda.html
The file was modified web/entries/GraphMarkingIBP.html
The file was modified web/entries/Graph_Saturation.html
The file was modified web/entries/Graph_Theory.html
The file was modified web/entries/Green.html
The file was modified web/entries/Groebner_Bases.html
The file was modified web/entries/Groebner_Macaulay.html
The file was modified web/entries/Gromov_Hyperbolicity.html
The file was modified web/entries/Grothendieck_Schemes.html
The file was modified web/entries/Group-Ring-Module.html
The file was modified web/entries/HOL-CSP.html
The file was modified web/entries/HOLCF-Prelude.html
The file was modified web/entries/HRB-Slicing.html
The file was modified web/entries/Hahn_Jordan_Decomposition.html
The file was modified web/entries/Hales_Jewett.html
The file was modified web/entries/Heard_Of.html
The file was modified web/entries/Hello_World.html
The file was modified web/entries/HereditarilyFinite.html
The file was modified web/entries/Hermite.html
The file was modified web/entries/Hermite_Lindemann.html
The file was modified web/entries/Hidden_Markov_Models.html
The file was modified web/entries/Higher_Order_Terms.html
The file was modified web/entries/Hoare_Time.html
The file was modified web/entries/Hood_Melville_Queue.html
The file was modified web/entries/HotelKeyCards.html
The file was modified web/entries/Huffman.html
The file was modified web/entries/Hybrid_Logic.html
The file was modified web/entries/Hybrid_Multi_Lane_Spatial_Logic.html
The file was modified web/entries/Hybrid_Systems_VCs.html
The file was modified web/entries/HyperCTL.html
The file was modified web/entries/Hyperdual.html
The file was modified web/entries/IEEE_Floating_Point.html
The file was modified web/entries/IFC_Tracking.html
The file was modified web/entries/IMAP-CRDT.html
The file was modified web/entries/IMO2019.html
The file was modified web/entries/IMP2.html
The file was modified web/entries/IMP2_Binary_Heap.html
The file was modified web/entries/IMP_Compiler.html
The file was modified web/entries/IMP_Compiler_Reuse.html
The file was modified web/entries/IP_Addresses.html
The file was modified web/entries/Imperative_Insertion_Sort.html
The file was modified web/entries/Implicational_Logic.html
The file was modified web/entries/Impossible_Geometry.html
The file was modified web/entries/Incompleteness.html
The file was modified web/entries/Incredible_Proof_Machine.html
The file was modified web/entries/Independence_CH.html
The file was modified web/entries/Inductive_Confidentiality.html
The file was modified web/entries/Inductive_Inference.html
The file was modified web/entries/InfPathElimination.html
The file was modified web/entries/InformationFlowSlicing.html
The file was modified web/entries/InformationFlowSlicing_Inter.html
The file was modified web/entries/Integration.html
The file was modified web/entries/Interpolation_Polynomials_HOL_Algebra.html
The file was modified web/entries/Interpreter_Optimizations.html
The file was modified web/entries/Interval_Arithmetic_Word32.html
The file was modified web/entries/Intro_Dest_Elim.html
The file was modified web/entries/Involutions2Squares.html
The file was modified web/entries/Iptables_Semantics.html
The file was modified web/entries/Irrational_Series_Erdos_Straus.html
The file was modified web/entries/Irrationality_J_Hancl.html
The file was modified web/entries/Irrationals_From_THEBOOK.html
The file was modified web/entries/IsaGeoCoq.html
The file was modified web/entries/IsaNet.html
The file was modified web/entries/Isabelle_C.html
The file was modified web/entries/Isabelle_Marries_Dirac.html
The file was modified web/entries/Isabelle_Meta_Model.html
The file was modified web/entries/Jacobson_Basic_Algebra.html
The file was modified web/entries/Jinja.html
The file was modified web/entries/JinjaDCI.html
The file was modified web/entries/JinjaThreads.html
The file was modified web/entries/JiveDataStoreModel.html
The file was modified web/entries/Jordan_Hoelder.html
The file was modified web/entries/Jordan_Normal_Form.html
The file was modified web/entries/KAD.html
The file was modified web/entries/KAT_and_DRA.html
The file was modified web/entries/KBPs.html
The file was modified web/entries/KD_Tree.html
The file was modified web/entries/Key_Agreement_Strong_Adversaries.html
The file was modified web/entries/Khovanskii_Theorem.html
The file was modified web/entries/Kleene_Algebra.html
The file was modified web/entries/Knights_Tour.html
The file was modified web/entries/Knot_Theory.html
The file was modified web/entries/Knuth_Bendix_Order.html
The file was modified web/entries/Knuth_Morris_Pratt.html
The file was modified web/entries/Koenigsberg_Friendship.html
The file was modified web/entries/Kruskal.html
The file was modified web/entries/Kuratowski_Closure_Complement.html
The file was modified web/entries/LLL_Basis_Reduction.html
The file was modified web/entries/LLL_Factorization.html
The file was modified web/entries/LOFT.html
The file was modified web/entries/LP_Duality.html
The file was modified web/entries/LTL.html
The file was modified web/entries/LTL_Master_Theorem.html
The file was modified web/entries/LTL_Normal_Form.html
The file was modified web/entries/LTL_to_DRA.html
The file was modified web/entries/LTL_to_GBA.html
The file was modified web/entries/Lam-ml-Normalization.html
The file was modified web/entries/LambdaAuth.html
The file was modified web/entries/LambdaMu.html
The file was modified web/entries/Lambda_Free_EPO.html
The file was modified web/entries/Lambda_Free_KBOs.html
The file was modified web/entries/Lambda_Free_RPOs.html
The file was modified web/entries/Lambert_W.html
The file was modified web/entries/Landau_Symbols.html
The file was modified web/entries/Laplace_Transform.html
The file was modified web/entries/Latin_Square.html
The file was modified web/entries/LatticeProperties.html
The file was modified web/entries/Launchbury.html
The file was modified web/entries/Laws_of_Large_Numbers.html
The file was modified web/entries/Lazy-Lists-II.html
The file was modified web/entries/Lazy_Case.html
The file was modified web/entries/Lehmer.html
The file was modified web/entries/Lifting_Definition_Option.html
The file was modified web/entries/Lifting_the_Exponent.html
The file was modified web/entries/LightweightJava.html
The file was modified web/entries/LinearQuantifierElim.html
The file was modified web/entries/Linear_Inequalities.html
The file was modified web/entries/Linear_Programming.html
The file was modified web/entries/Linear_Recurrences.html
The file was modified web/entries/Liouville_Numbers.html
The file was modified web/entries/List-Index.html
The file was modified web/entries/List-Infinite.html
The file was modified web/entries/List_Interleaving.html
The file was modified web/entries/List_Inversions.html
The file was modified web/entries/List_Update.html
The file was modified web/entries/LocalLexing.html
The file was modified web/entries/Localization_Ring.html
The file was modified web/entries/Locally-Nameless-Sigma.html
The file was modified web/entries/Logging_Independent_Anonymity.html
The file was modified web/entries/Lowe_Ontological_Argument.html
The file was modified web/entries/Lower_Semicontinuous.html
The file was modified web/entries/Lp.html
The file was modified web/entries/Lucas_Theorem.html
The file was modified web/entries/MDP-Algorithms.html
The file was modified web/entries/MDP-Rewards.html
The file was modified web/entries/MFMC_Countable.html
The file was modified web/entries/MFODL_Monitor_Optimized.html
The file was modified web/entries/MFOTL_Monitor.html
The file was modified web/entries/MSO_Regex_Equivalence.html
The file was modified web/entries/Markov_Models.html
The file was modified web/entries/Marriage.html
The file was modified web/entries/Mason_Stothers.html
The file was modified web/entries/Matrices_for_ODEs.html
The file was modified web/entries/Matrix.html
The file was modified web/entries/Matrix_Tensor.html
The file was modified web/entries/Matroids.html
The file was modified web/entries/Max-Card-Matching.html
The file was modified web/entries/Median_Method.html
The file was modified web/entries/Median_Of_Medians_Selection.html
The file was modified web/entries/Menger.html
The file was modified web/entries/Mereology.html
The file was modified web/entries/Mersenne_Primes.html
The file was modified web/entries/Metalogic_ProofChecker.html
The file was modified web/entries/MiniML.html
The file was modified web/entries/MiniSail.html
The file was modified web/entries/Minimal_SSA.html
The file was modified web/entries/Minkowskis_Theorem.html
The file was modified web/entries/Minsky_Machines.html
The file was modified web/entries/Modal_Logics_for_NTS.html
The file was modified web/entries/Modular_Assembly_Kit_Security.html
The file was modified web/entries/Modular_arithmetic_LLL_and_HNF_algorithms.html
The file was modified web/entries/Monad_Memo_DP.html
The file was modified web/entries/Monad_Normalisation.html
The file was modified web/entries/MonoBoolTranAlgebra.html
The file was modified web/entries/MonoidalCategory.html
The file was modified web/entries/Monomorphic_Monad.html
The file was modified web/entries/MuchAdoAboutTwo.html
The file was modified web/entries/Multi_Party_Computation.html
The file was modified web/entries/Multirelations.html
The file was modified web/entries/Multiset_Ordering_NPC.html
The file was modified web/entries/Myhill-Nerode.html
The file was modified web/entries/Name_Carrying_Type_Inference.html
The file was modified web/entries/Nano_JSON.html
The file was modified web/entries/Nash_Williams.html
The file was modified web/entries/Nat-Interval-Logic.html
The file was modified web/entries/Native_Word.html
The file was modified web/entries/Nested_Multisets_Ordinals.html
The file was modified web/entries/Network_Security_Policy_Verification.html
The file was modified web/entries/Neumann_Morgenstern_Utility.html
The file was modified web/entries/No_FTL_observers.html
The file was modified web/entries/Nominal2.html
The file was modified web/entries/Noninterference_CSP.html
The file was modified web/entries/Noninterference_Concurrent_Composition.html
The file was modified web/entries/Noninterference_Generic_Unwinding.html
The file was modified web/entries/Noninterference_Inductive_Unwinding.html
The file was modified web/entries/Noninterference_Ipurge_Unwinding.html
The file was modified web/entries/Noninterference_Sequential_Composition.html
The file was modified web/entries/NormByEval.html
The file was modified web/entries/Nullstellensatz.html
The file was modified web/entries/Number_Theoretic_Transform.html
The file was modified web/entries/Octonions.html
The file was modified web/entries/OpSets.html
The file was modified web/entries/Open_Induction.html
The file was modified web/entries/Optics.html
The file was modified web/entries/Optimal_BST.html
The file was modified web/entries/Orbit_Stabiliser.html
The file was modified web/entries/Order_Lattice_Props.html
The file was modified web/entries/Ordered_Resolution_Prover.html
The file was modified web/entries/Ordinal.html
The file was modified web/entries/Ordinal_Partitions.html
The file was modified web/entries/Ordinals_and_Cardinals.html
The file was modified web/entries/Ordinary_Differential_Equations.html
The file was modified web/entries/PAC_Checker.html
The file was modified web/entries/PAL.html
The file was modified web/entries/PCF.html
The file was modified web/entries/PLM.html
The file was modified web/entries/POPLmark-deBruijn.html
The file was modified web/entries/PSemigroupsConvolution.html
The file was modified web/entries/Package_logic.html
The file was modified web/entries/Padic_Field.html
The file was modified web/entries/Padic_Ints.html
The file was modified web/entries/Pairing_Heap.html
The file was modified web/entries/Paraconsistency.html
The file was modified web/entries/Parity_Game.html
The file was modified web/entries/Partial_Function_MR.html
The file was modified web/entries/Partial_Order_Reduction.html
The file was modified web/entries/Password_Authentication_Protocol.html
The file was modified web/entries/Pell.html
The file was modified web/entries/Perfect-Number-Thm.html
The file was modified web/entries/Perron_Frobenius.html
The file was modified web/entries/Physical_Quantities.html
The file was modified web/entries/Pi_Calculus.html
The file was modified web/entries/Pi_Transcendental.html
The file was modified web/entries/Planarity_Certificates.html
The file was modified web/entries/Pluennecke_Ruzsa_Inequality.html
The file was modified web/entries/Poincare_Bendixson.html
The file was modified web/entries/Poincare_Disc.html
The file was modified web/entries/Polynomial_Factorization.html
The file was modified web/entries/Polynomial_Interpolation.html
The file was modified web/entries/Polynomials.html
The file was modified web/entries/Pop_Refinement.html
The file was modified web/entries/Posix-Lexing.html
The file was modified web/entries/Possibilistic_Noninterference.html
The file was modified web/entries/Power_Sum_Polynomials.html
The file was modified web/entries/Pratt_Certificate.html
The file was modified web/entries/Prefix_Free_Code_Combinators.html
The file was modified web/entries/Presburger-Automata.html
The file was modified web/entries/Prim_Dijkstra_Simple.html
The file was modified web/entries/Prime_Distribution_Elementary.html
The file was modified web/entries/Prime_Harmonic_Series.html
The file was modified web/entries/Prime_Number_Theorem.html
The file was modified web/entries/Priority_Queue_Braun.html
The file was modified web/entries/Priority_Search_Trees.html
The file was modified web/entries/Probabilistic_Noninterference.html
The file was modified web/entries/Probabilistic_Prime_Tests.html
The file was modified web/entries/Probabilistic_System_Zoo.html
The file was modified web/entries/Probabilistic_Timed_Automata.html
The file was modified web/entries/Probabilistic_While.html
The file was modified web/entries/Program-Conflict-Analysis.html
The file was modified web/entries/Progress_Tracking.html
The file was modified web/entries/Projective_Geometry.html
The file was modified web/entries/Projective_Measurements.html
The file was modified web/entries/Promela.html
The file was modified web/entries/Proof_Strategy_Language.html
The file was modified web/entries/PropResPI.html
The file was modified web/entries/Propositional_Proof_Systems.html
The file was modified web/entries/Prpu_Maxflow.html
The file was modified web/entries/PseudoHoops.html
The file was modified web/entries/Psi_Calculi.html
The file was modified web/entries/Ptolemys_Theorem.html
The file was modified web/entries/Public_Announcement_Logic.html
The file was modified web/entries/QHLProver.html
The file was modified web/entries/QR_Decomposition.html
The file was modified web/entries/Quantales.html
The file was modified web/entries/Quasi_Borel_Spaces.html
The file was modified web/entries/Quaternions.html
The file was modified web/entries/Quick_Sort_Cost.html
The file was modified web/entries/RIPEMD-160-SPARK.html
The file was modified web/entries/ROBDD.html
The file was modified web/entries/RSAPSS.html
The file was modified web/entries/Ramsey-Infinite.html
The file was modified web/entries/Random_BSTs.html
The file was modified web/entries/Random_Graph_Subgraph_Threshold.html
The file was modified web/entries/Randomised_BSTs.html
The file was modified web/entries/Randomised_Social_Choice.html
The file was modified web/entries/Rank_Nullity_Theorem.html
The file was modified web/entries/Real_Impl.html
The file was modified web/entries/Real_Power.html
The file was modified web/entries/Real_Time_Deque.html
The file was modified web/entries/Recursion-Addition.html
The file was modified web/entries/Recursion-Theory-I.html
The file was modified web/entries/Refine_Imperative_HOL.html
The file was modified web/entries/Refine_Monadic.html
The file was modified web/entries/RefinementReactive.html
The file was modified web/entries/Regex_Equivalence.html
The file was modified web/entries/Registers.html
The file was modified web/entries/Regression_Test_Selection.html
The file was modified web/entries/Regular-Sets.html
The file was modified web/entries/Regular_Algebras.html
The file was modified web/entries/Regular_Tree_Relations.html
The file was modified web/entries/Relation_Algebra.html
The file was modified web/entries/Relational-Incorrectness-Logic.html
The file was modified web/entries/Relational_Disjoint_Set_Forests.html
The file was modified web/entries/Relational_Forests.html
The file was modified web/entries/Relational_Method.html
The file was modified web/entries/Relational_Minimum_Spanning_Trees.html
The file was modified web/entries/Relational_Paths.html
The file was modified web/entries/Rep_Fin_Groups.html
The file was modified web/entries/ResiduatedTransitionSystem.html
The file was modified web/entries/Residuated_Lattices.html
The file was modified web/entries/Resolution_FOL.html
The file was modified web/entries/Rewrite_Properties_Reduction.html
The file was modified web/entries/Rewriting_Z.html
The file was modified web/entries/Ribbon_Proofs.html
The file was modified web/entries/Risk_Free_Lending.html
The file was modified web/entries/Robbins-Conjecture.html
The file was modified web/entries/Robinson_Arithmetic.html
The file was modified web/entries/Root_Balanced_Tree.html
The file was modified web/entries/Roth_Arithmetic_Progressions.html
The file was modified web/entries/Routing.html
The file was modified web/entries/Roy_Floyd_Warshall.html
The file was modified web/entries/SATSolverVerification.html
The file was modified web/entries/SCC_Bloemen_Sequential.html
The file was modified web/entries/SC_DOM_Components.html
The file was modified web/entries/SDS_Impossibility.html
The file was modified web/entries/SIFPL.html
The file was modified web/entries/SIFUM_Type_Systems.html
The file was modified web/entries/SPARCv8.html
The file was modified web/entries/Safe_Distance.html
The file was modified web/entries/Safe_OCL.html
The file was modified web/entries/Saturation_Framework.html
The file was modified web/entries/Saturation_Framework_Extensions.html
The file was modified web/entries/Schutz_Spacetime.html
The file was modified web/entries/Secondary_Sylow.html
The file was modified web/entries/Security_Protocol_Refinement.html
The file was modified web/entries/Selection_Heap_Sort.html
The file was modified web/entries/SenSocialChoice.html
The file was modified web/entries/Separata.html
The file was modified web/entries/Separation_Algebra.html
The file was modified web/entries/Separation_Logic_Imperative_HOL.html
The file was modified web/entries/Separation_Logic_Unbounded.html
The file was modified web/entries/SequentInvertibility.html
The file was modified web/entries/Shadow_DOM.html
The file was modified web/entries/Shadow_SC_DOM.html
The file was modified web/entries/Shivers-CFA.html
The file was modified web/entries/ShortestPath.html
The file was modified web/entries/Show.html
The file was modified web/entries/Sigma_Commit_Crypto.html
The file was modified web/entries/Signature_Groebner.html
The file was modified web/entries/Simpl.html
The file was modified web/entries/Simple_Firewall.html
The file was modified web/entries/Simplex.html
The file was modified web/entries/Simplicial_complexes_and_boolean_functions.html
The file was modified web/entries/SimplifiedOntologicalArgument.html
The file was modified web/entries/Skew_Heap.html
The file was modified web/entries/Skip_Lists.html
The file was modified web/entries/Slicing.html
The file was modified web/entries/Sliding_Window_Algorithm.html
The file was modified web/entries/Smith_Normal_Form.html
The file was modified web/entries/Smooth_Manifolds.html
The file was modified web/entries/Solidity.html
The file was modified web/entries/Sophomores_Dream.html
The file was modified web/entries/Sort_Encodings.html
The file was modified web/entries/Source_Coding_Theorem.html
The file was modified web/entries/SpecCheck.html
The file was modified web/entries/Special_Function_Bounds.html
The file was modified web/entries/Splay_Tree.html
The file was modified web/entries/Sqrt_Babylonian.html
The file was modified web/entries/Stable_Matching.html
The file was modified web/entries/Stalnaker_Logic.html
The file was modified web/entries/Statecharts.html
The file was modified web/entries/Stateful_Protocol_Composition_and_Typing.html
The file was modified web/entries/Stellar_Quorums.html
The file was modified web/entries/Stern_Brocot.html
The file was modified web/entries/Stewart_Apollonius.html
The file was modified web/entries/Stirling_Formula.html
The file was modified web/entries/Stochastic_Matrices.html
The file was modified web/entries/Stone_Algebras.html
The file was modified web/entries/Stone_Kleene_Relation_Algebras.html
The file was modified web/entries/Stone_Relation_Algebras.html
The file was modified web/entries/Store_Buffer_Reduction.html
The file was modified web/entries/Stream-Fusion.html
The file was modified web/entries/Stream_Fusion_Code.html
The file was modified web/entries/Strong_Security.html
The file was modified web/entries/Sturm_Sequences.html
The file was modified web/entries/Sturm_Tarski.html
The file was modified web/entries/Stuttering_Equivalence.html
The file was modified web/entries/Subresultants.html
The file was modified web/entries/Subset_Boolean_Algebras.html
The file was modified web/entries/SumSquares.html
The file was modified web/entries/Sunflowers.html
The file was modified web/entries/SuperCalc.html
The file was modified web/entries/Surprise_Paradox.html
The file was modified web/entries/Symmetric_Polynomials.html
The file was modified web/entries/Syntax_Independent_Logic.html
The file was modified web/entries/Szemeredi_Regularity.html
The file was modified web/entries/Szpilrajn.html
The file was modified web/entries/TESL_Language.html
The file was modified web/entries/TLA.html
The file was modified web/entries/Tail_Recursive_Functions.html
The file was modified web/entries/Tarskis_Geometry.html
The file was modified web/entries/Taylor_Models.html
The file was modified web/entries/Three_Circles.html
The file was modified web/entries/Timed_Automata.html
The file was modified web/entries/Topological_Semantics.html
The file was modified web/entries/Topology.html
The file was modified web/entries/TortoiseHare.html
The file was modified web/entries/Transcendence_Series_Hancl_Rucki.html
The file was modified web/entries/Transformer_Semantics.html
The file was modified web/entries/Transition_Systems_and_Automata.html
The file was modified web/entries/Transitive-Closure-II.html
The file was modified web/entries/Transitive-Closure.html
The file was modified web/entries/Transitive_Models.html
The file was modified web/entries/Treaps.html
The file was modified web/entries/Tree-Automata.html
The file was modified web/entries/Tree_Decomposition.html
The file was modified web/entries/Triangle.html
The file was modified web/entries/Trie.html
The file was modified web/entries/Twelvefold_Way.html
The file was modified web/entries/Tycon.html
The file was modified web/entries/Types_Tableaus_and_Goedels_God.html
The file was modified web/entries/Types_To_Sets_Extension.html
The file was modified web/entries/UPF.html
The file was modified web/entries/UPF_Firewall.html
The file was modified web/entries/UTP.html
The file was modified web/entries/Universal_Hash_Families.html
The file was modified web/entries/Universal_Turing_Machine.html
The file was modified web/entries/UpDown_Scheme.html
The file was modified web/entries/VYDRA_MDL.html
The file was modified web/entries/Valuation.html
The file was modified web/entries/Van_Emde_Boas_Trees.html
The file was modified web/entries/Van_der_Waerden.html
The file was modified web/entries/VectorSpace.html
The file was modified web/entries/VeriComp.html
The file was modified web/entries/Verified-Prover.html
The file was modified web/entries/Verified_SAT_Based_AI_Planning.html
The file was modified web/entries/VerifyThis2018.html
The file was modified web/entries/VerifyThis2019.html
The file was modified web/entries/Vickrey_Clarke_Groves.html
The file was modified web/entries/Virtual_Substitution.html
The file was modified web/entries/VolpanoSmith.html
The file was modified web/entries/WHATandWHERE_Security.html
The file was modified web/entries/WOOT_Strong_Eventual_Consistency.html
The file was modified web/entries/WebAssembly.html
The file was modified web/entries/Weight_Balanced_Trees.html
The file was modified web/entries/Weighted_Arithmetic_Geometric_Mean.html
The file was modified web/entries/Weighted_Path_Order.html
The file was modified web/entries/Well_Quasi_Orders.html
The file was modified web/entries/Wetzels_Problem.html
The file was modified web/entries/Winding_Number_Eval.html
The file was modified web/entries/Word_Lib.html
The file was modified web/entries/WorkerWrapper.html
The file was modified web/entries/X86_Semantics.html
The file was modified web/entries/XML.html
The file was modified web/entries/Youngs_Inequality.html
The file was modified web/entries/ZFC_in_HOL.html
The file was modified web/entries/Zeta_3_Irrational.html
The file was modified web/entries/Zeta_Function.html
The file was modified web/entries/pGCL.html
The file was modified web/index.xml
The file was modified web/statistics/index.html
The file was modified web/submission/index.html
The file was modified web/topics/computer-science/algorithms/approximation/index.html
The file was modified web/topics/computer-science/algorithms/concurrent/index.html
The file was modified web/topics/computer-science/algorithms/distributed/index.html
The file was modified web/topics/computer-science/algorithms/graph/index.html
The file was modified web/topics/computer-science/algorithms/index.html
The file was modified web/topics/computer-science/algorithms/online/index.html
The file was modified web/topics/computer-science/algorithms/optimization/index.html
The file was modified web/topics/computer-science/algorithms/quantum-computing/index.html
The file was modified web/topics/computer-science/artificial-intelligence/index.html
The file was modified web/topics/computer-science/automata-and-formal-languages/index.html
The file was modified web/topics/computer-science/concurrency/index.html
The file was modified web/topics/computer-science/concurrency/process-calculi/index.html
The file was modified web/topics/computer-science/data-structures/index.html
The file was modified web/topics/computer-science/functional-programming/index.html
The file was modified web/topics/computer-science/hardware/index.html
The file was modified web/topics/computer-science/machine-learning/index.html
The file was modified web/topics/computer-science/networks/index.html
The file was modified web/topics/computer-science/programming-languages/compiling/index.html
The file was modified web/topics/computer-science/programming-languages/index.html
The file was modified web/topics/computer-science/programming-languages/lambda-calculi/index.html
The file was modified web/topics/computer-science/programming-languages/language-definitions/index.html
The file was modified web/topics/computer-science/programming-languages/logics/index.html
The file was modified web/topics/computer-science/programming-languages/static-analysis/index.html
The file was modified web/topics/computer-science/programming-languages/type-systems/index.html
The file was modified web/topics/computer-science/security/cryptography/index.html
The file was modified web/topics/computer-science/security/index.html
The file was modified web/topics/computer-science/semantics-and-reasoning/index.html
The file was modified web/topics/computer-science/system-description-languages/index.html
The file was modified web/topics/logic/computability/index.html
The file was modified web/topics/logic/general-logic/classical-first-order-logic/index.html
The file was modified web/topics/logic/general-logic/classical-propositional-logic/index.html
The file was modified web/topics/logic/general-logic/decidability-of-theories/index.html
The file was modified web/topics/logic/general-logic/index.html
The file was modified web/topics/logic/general-logic/logics-of-knowledge-and-belief/index.html
The file was modified web/topics/logic/general-logic/mechanization-of-proofs/index.html
The file was modified web/topics/logic/general-logic/modal-logic/index.html
The file was modified web/topics/logic/general-logic/paraconsistent-logics/index.html
The file was modified web/topics/logic/general-logic/temporal-logic/index.html
The file was modified web/topics/logic/philosophical-aspects/index.html
The file was modified web/topics/logic/proof-theory/index.html
The file was modified web/topics/logic/rewriting/index.html
The file was modified web/topics/logic/set-theory/index.html
The file was modified web/topics/mathematics/algebra/index.html
The file was modified web/topics/mathematics/analysis/index.html
The file was modified web/topics/mathematics/category-theory/index.html
The file was modified web/topics/mathematics/combinatorics/index.html
The file was modified web/topics/mathematics/games-and-economics/index.html
The file was modified web/topics/mathematics/geometry/index.html
The file was modified web/topics/mathematics/graph-theory/index.html
The file was modified web/topics/mathematics/measure-and-integration/index.html
The file was modified web/topics/mathematics/number-theory/index.html
The file was modified web/topics/mathematics/order/index.html
The file was modified web/topics/mathematics/physics/index.html
The file was modified web/topics/mathematics/physics/quantum-information/index.html
The file was modified web/topics/mathematics/probability-theory/index.html
The file was modified web/topics/mathematics/topology/index.html
Changeset 13050:c1bc44c10400 by fabian huch _huch@in.tum.de_:
afp site: minor stylistic improvements;
The file was modified admin/site/content/submission.md
The file was modified admin/site/themes/afp/assets/sass/main.scss
The file was modified admin/site/themes/afp/layouts/entries/single.html
The file was modified admin/site/themes/afp/layouts/shortcodes/statistics.html
The file was modified admin/site/themes/afp/layouts/topics/list.html
The file was modified metadata/topics.toml
Changeset 13049:43747de4292f by rene thiemann _rene.thiemann@uibk.ac.at_:
web entry for Stalnaker_Logic
The file was addedmetadata/entries/Stalnaker_Logic.toml
The file was addedweb/authors/guzman/index.html
The file was addedweb/authors/guzman/index.xml
The file was addedweb/entries/Stalnaker_Logic.html
The file was addedweb/theories/stalnaker_logic/index.html
The file was modified metadata/authors.toml
The file was modified web/authors/index.html
The file was modified web/authors/index.json
The file was modified web/data/keywords.json
The file was modified web/dependencies/epistemic_logic/index.html
The file was modified web/dependencies/epistemic_logic/index.xml
The file was modified web/dependencies/index.html
The file was modified web/entries/Epistemic_Logic.html
The file was modified web/entries/Public_Announcement_Logic.html
The file was modified web/entries/index.html
The file was modified web/entries/index.xml
The file was modified web/index.html
The file was modified web/index.json
The file was modified web/index.xml
The file was modified web/sitemap.xml
The file was modified web/statistics/index.html
The file was modified web/theories/index.xml
The file was modified web/topics/index.html
The file was modified web/topics/logic/general-logic/index.html
The file was modified web/topics/logic/general-logic/index.xml
The file was modified web/topics/logic/general-logic/logics-of-knowledge-and-belief/index.html
The file was modified web/topics/logic/general-logic/logics-of-knowledge-and-belief/index.xml
Changeset 13048:e9bab02fb67c by rene thiemann _rene.thiemann@uibk.ac.at_:
new entry: Stalnaker Logic
The file was addedthys/Stalnaker_Logic/ROOT
The file was addedthys/Stalnaker_Logic/Stalnaker_Logic.thy
The file was addedthys/Stalnaker_Logic/document/root.bib
The file was addedthys/Stalnaker_Logic/document/root.tex
The file was modified thys/ROOTS
Changeset 13047:a969a9029a5c by wenzelm:
clarified options, following f2094906e491;
The file was modified thys/Sturm_Sequences/ROOT