Changes

Changes from Mercurial (hg https://bitbucket.org/isa-afp/afp-devel/ default)

Summary

uniform ASCII and non-ASCII notation
Added missing file.
More material for Stirling_Formula
Improve readability of document for Differential_Dynamic_Logic

Changeset 7648:2ea64cb09ca6 by fleury _mathias.fleury@mpi-inf.mpg.de_: uniform ASCII and non-ASCII notation
The file was modified	`thys/Nested_Multisets_Ordinals/Signed_Multiset.thy`
Changeset 7647:e3384d6906aa by eberlm _eberlm@in.tum.de_: Added missing file.
The file was added	`thys/Stirling_Formula/Ln_Gamma_Asymptotics.thy`
Changeset 7646:a2bea9b61de9 by eberlm _eberlm@in.tum.de_: More material for Stirling_Formula
The file was modified	`thys/Stirling_Formula/ROOT`
The file was modified	`thys/Stirling_Formula/Stirling_Formula.thy`
The file was modified	`thys/Stirling_Formula/document/root.bib`
The file was modified	`thys/Stirling_Formula/document/root.tex`
Changeset 7645:20d2a76c2d99 by bbohrer@cs.cmu.edu: Improve readability of document for Differential_Dynamic_Logic
The file was modified	`thys/Differential_Dynamic_Logic/Axioms.thy`
The file was modified	`thys/Differential_Dynamic_Logic/Bound_Effect.thy`
The file was modified	`thys/Differential_Dynamic_Logic/Coincidence.thy`
The file was modified	`thys/Differential_Dynamic_Logic/Denotational_Semantics.thy`
The file was modified	`thys/Differential_Dynamic_Logic/Differential_Axioms.thy`
The file was modified	`thys/Differential_Dynamic_Logic/Differential_Dynamic_Logic.thy`
The file was modified	`thys/Differential_Dynamic_Logic/Frechet_Correctness.thy`
The file was modified	`thys/Differential_Dynamic_Logic/Ids.thy`
The file was modified	`thys/Differential_Dynamic_Logic/Lib.thy`
The file was modified	`thys/Differential_Dynamic_Logic/Pretty_Printer.thy`
The file was modified	`thys/Differential_Dynamic_Logic/Proof_Checker.thy`
The file was modified	`thys/Differential_Dynamic_Logic/Static_Semantics.thy`
The file was modified	`thys/Differential_Dynamic_Logic/Syntax.thy`
The file was modified	`thys/Differential_Dynamic_Logic/USubst.thy`
The file was modified	`thys/Differential_Dynamic_Logic/USubst_Lemma.thy`
The file was modified	`thys/Differential_Dynamic_Logic/Uniform_Renaming.thy`
The file was modified	`thys/Differential_Dynamic_Logic/document/root.bib`
The file was modified	`thys/Differential_Dynamic_Logic/document/root.tex`

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

Summary

use the cancellation simprocs directly
don't activate simproc on cancel_comm_monoid_add

Changeset 65031:52e2c99f3711 by fleury _mathias.fleury@mpi-inf.mpg.de_: use the cancellation simprocs directly
The file was modified	`src/HOL/Library/Multiset.thy`
The file was modified	`src/HOL/Library/Multiset_Order.thy`
The file was removed	`src/HOL/Library/multiset_order_simprocs.ML`
Changeset 65030:7fd4130cd0a4 by fleury _mathias.fleury@mpi-inf.mpg.de_: don't activate simproc on cancel_comm_monoid_add
The file was modified	`src/HOL/Library/Cancellation.thy`