Skip to content
[Jenkins]Jenkins
log in
Success

Changes

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

Summary

  1. tuned BNF bounds for function space and bounded sets; NEWS and CONTRIBUTORS
  2. strict bounds for BNFs (by Jan van Brügge)
Changeset 75625:0dd3ac5fdbaa by traytel:
tuned BNF bounds for function space and bounded sets; NEWS and CONTRIBUTORS
The file was modified CONTRIBUTORS
The file was modified NEWS
The file was modified src/Doc/Datatypes/Datatypes.thy
The file was modified src/HOL/BNF_Cardinal_Arithmetic.thy
The file was modified src/HOL/Basic_BNFs.thy
The file was modified src/HOL/Cardinals/Bounded_Set.thy
The file was modified src/HOL/Library/Countable_Set_Type.thy
The file was modified src/HOL/Probability/Probability_Mass_Function.thy
The file was modified src/HOL/Tools/BNF/bnf_comp_tactics.ML
The file was modified src/HOL/Tools/BNF/bnf_gfp.ML
Changeset 75624:22d1c5f2b9f4 by traytel:
strict bounds for BNFs (by Jan van Brügge)
The file was modified src/Doc/Datatypes/Datatypes.thy
The file was modified src/HOL/BNF_Cardinal_Arithmetic.thy
The file was modified src/HOL/BNF_Cardinal_Order_Relation.thy
The file was modified src/HOL/BNF_Composition.thy
The file was modified src/HOL/BNF_Greatest_Fixpoint.thy
The file was modified src/HOL/BNF_Wellorder_Constructions.thy
The file was modified src/HOL/BNF_Wellorder_Relation.thy
The file was modified src/HOL/Basic_BNFs.thy
The file was modified src/HOL/Cardinals/Bounded_Set.thy
The file was modified src/HOL/Cardinals/Cardinal_Order_Relation.thy
The file was modified src/HOL/Cardinals/Fun_More.thy
The file was modified src/HOL/Cardinals/Wellorder_Constructions.thy
The file was modified src/HOL/Fun.thy
The file was modified src/HOL/Library/Countable_Set_Type.thy
The file was modified src/HOL/Library/FSet.thy
The file was modified src/HOL/Library/Multiset.thy
The file was modified src/HOL/Library/Uprod.thy
The file was modified src/HOL/Probability/Probability_Mass_Function.thy
The file was modified src/HOL/Tools/BNF/bnf_comp.ML
The file was modified src/HOL/Tools/BNF/bnf_comp_tactics.ML
The file was modified src/HOL/Tools/BNF/bnf_def.ML
The file was modified src/HOL/Tools/BNF/bnf_fp_util.ML
The file was modified src/HOL/Tools/BNF/bnf_gfp.ML
The file was modified src/HOL/Tools/BNF/bnf_gfp_tactics.ML
The file was modified src/HOL/Tools/BNF/bnf_gfp_util.ML
The file was modified src/HOL/Tools/BNF/bnf_lfp.ML
The file was modified src/HOL/Tools/BNF/bnf_lfp_tactics.ML
The file was modified src/HOL/Tools/BNF/bnf_lift.ML
The file was modified src/HOL/Tools/BNF/bnf_util.ML

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

Summary

  1. merged
  2. tuned BNF bound
  3. strict bounds for BNFs (by Jan van Brügge)
Changeset 12739:969d123ac0b9 by traytel:
merged
Changeset 12738:2500a913c1f2 by traytel:
tuned BNF bound
The file was modified thys/BNF_Operations/GFP.thy
The file was modified thys/Probabilistic_System_Zoo/Finitely_Bounded_Set_Counterexample.thy
The file was modified thys/Probabilistic_System_Zoo/Nonempty_Bounded_Set.thy
Changeset 12737:5b2658c54443 by traytel:
strict bounds for BNFs (by Jan van Brügge)
The file was modified thys/BNF_CC/Axiomatised_BNF_CC.thy
The file was modified thys/BNF_CC/Composition.thy
The file was modified thys/BNF_CC/Subtypes.thy
The file was modified thys/BNF_Operations/Compose.thy
The file was modified thys/BNF_Operations/GFP.thy
The file was modified thys/BNF_Operations/Kill.thy
The file was modified thys/BNF_Operations/LFP.thy
The file was modified thys/BNF_Operations/Lift.thy
The file was modified thys/BNF_Operations/Permute.thy
The file was modified thys/Probabilistic_System_Zoo/Bool_Bounded_Set.thy
The file was modified thys/Probabilistic_System_Zoo/Finitely_Bounded_Set_Counterexample.thy
The file was modified thys/Probabilistic_System_Zoo/Nonempty_Bounded_Set.thy
The file was modified thys/Probabilistic_System_Zoo/Vardi_Counterexample.thy