Diffusion Isabelle e0237f2eb49d

Removed multiplicativity assumption from normalization_semidom
e0237f2eb49d
Actions

Tags

None

Subscribers

None

Description

Removed multiplicativity assumption from normalization_semidom

Details

Provenance

Authored on

Parents

rISABELLE028edb1e5b99: clarified file names;

Branches

Unknown

Tags

Unknown

Event Timeline

pruvisto committed rISABELLEe0237f2eb49d: Removed multiplicativity assumption from normalization_semidom.Jan 21 2020, 11:02 AM

pruvisto mentioned this in rAFP0f0adba767a3: adapted to isabelle-dev/e0237f2eb49d.Feb 12 2020, 10:57 PM

pruvisto mentioned this in rISABELLE2aa38099aa8c: updated NEWS w.r.t. e0237f2eb49d.Mar 10 2020, 2:18 PM

Changes (13)

Path

Size

src/

HOL/

Computational_Algebra/

Euclidean_Algorithm.thy

Factorial_Ring.thy

Field_as_Ring.thy

Formal_Power_Series.thy

Normalized_Fraction.thy

Polynomial_Factorial.thy

Library/

Number_Theory/

Prime_Powers.thy

rISABELLEe0237f2eb49d

src/HOL/Computational_Algebra/Euclidean_Algorithm.thy

Loading...

src/HOL/Computational_Algebra/Factorial_Ring.thy

Loading...

src/HOL/Computational_Algebra/Field_as_Ring.thy

Loading...

src/HOL/Computational_Algebra/Formal_Power_Series.thy

Loading...

src/HOL/Computational_Algebra/Normalized_Fraction.thy

Loading...

src/HOL/Computational_Algebra/Nth_Powers.thy

Loading...

src/HOL/Computational_Algebra/Polynomial.thy

Loading...

src/HOL/Computational_Algebra/Polynomial_Factorial.thy

Loading...

src/HOL/GCD.thy

Loading...

src/HOL/Library/Multiset.thy

Loading...

src/HOL/Number_Theory/Prime_Powers.thy

Loading...

src/HOL/Power.thy

Loading...

src/HOL/Rings.thy

Loading...