Diffusion Isabelle d52934f126d4

new formulation of an auxiliary lemma
d52934f126d4
Actions

Tags

None

Subscribers

None

Description

new formulation of an auxiliary lemma

Details

Provenance

florian.haftmann

Authored on

Parents

rISABELLEd900ff3f314a: A few more inclusion-exclusion theorems from HOL Light

Branches

Unknown

Tags

Unknown

Event Timeline

florian.haftmann committed rISABELLEd52934f126d4: new formulation of an auxiliary lemma.Sep 16 2023, 8:38 AM

Changes (4)

Path

Size

src/

HOL/

Euclidean_Rings.thy

Number_Theory/

Pocklington.thy

rISABELLEd52934f126d4

src/HOL/Divides.thy

Loading...

src/HOL/Euclidean_Rings.thy

Loading...

src/HOL/Number_Theory/Pocklington.thy

Loading...

src/HOL/Parity.thy

Loading...