Diffusion afp-devel a9d827f1c5b1

moved some theorems into HOL main corpus
a9d827f1c5b1
Actions

Tags

None

Subscribers

None

Description

moved some theorems into HOL main corpus

Details

Provenance

florian.haftmann

Authored on

Parents

rAFP65974f61a998: official fact collection sign_simps

Branches

Unknown

Tags

Unknown

Event Timeline

Changes (5)

Path

Size

thys/

Algebraic_Numbers/

Complex_Algebraic_Numbers.thy

Real_Algebraic_Numbers.thy

Gromov_Hyperbolicity/

Morse_Gromov_Theorem.thy

KD_Tree/

Sqrt_Babylonian/

Sqrt_Babylonian_Auxiliary.thy

rAFPa9d827f1c5b1

thys/Algebraic_Numbers/Complex_Algebraic_Numbers.thy

Loading...

thys/Algebraic_Numbers/Real_Algebraic_Numbers.thy

Loading...

thys/Gromov_Hyperbolicity/Morse_Gromov_Theorem.thy

Loading...

thys/KD_Tree/KDTree.thy

Loading...

thys/Sqrt_Babylonian/Sqrt_Babylonian_Auxiliary.thy

Loading...