Diffusion afp-devel c8d4f20a1071

64
c8d4f20a1071
Actions

Description

dedicated integration theory for word8/16/32/64

Details

Provenance

florian.haftmann

Authored on

Parents

rAFPd234f75be25a: tuned names

Branches

Unknown

Tags

Unknown

Event Timeline

florian.haftmann committed rAFPc8d4f20a1071: dedicated integration theory for word8/16/32/64.Nov 6 2020, 9:55 AM

Changes (16)

Path

Size

thys

Complx/

ex/

IEEE_Floating_Point/

	Word_32.thy
	Word_Lemmas_32.thy

	Word_64.thy
	Word_Lemmas_64.thy

rAFPc8d4f20a1071

View Options

thys/Complx/ex/SumArr.thy

View Options

thys/IEEE_Floating_Point/FP64.thy

View Options

thys/Word_Lib/Examples.thy

View Options

thys/Word_Lib/Guide.thy

View Options

thys/Word_Lib/Word_16.thy

View Options

thys/Word_Lib/Word_32.thy

View Options

thys/Word_Lib/Word_64.thy

View Options

thys/Word_Lib/Word_8.thy

View Options

thys/Word_Lib/Word_Lemmas_32.thy

View Options

thys/Word_Lib/Word_Lemmas_64.thy

View Options

thys/Word_Lib/Word_Lib_Sumo.thy

View Options

thys/Word_Lib/Word_Setup_32.thy

View Options

thys/Word_Lib/Word_Setup_64.thy

View Options

thys/Word_Lib/Word_Syntax.thy

dedicated integration theory for word8/16/32/64c8d4f20a1071Actions

Description

Details

Event Timeline

Changes (16)

rAFPc8d4f20a1071

thys/Complx/ex/SumArr.thy

thys/IEEE_Floating_Point/FP64.thy

thys/Word_Lib/Examples.thy

thys/Word_Lib/Guide.thy

thys/Word_Lib/Word_16.thy

thys/Word_Lib/Word_32.thy

thys/Word_Lib/Word_64.thy

thys/Word_Lib/Word_8.thy

thys/Word_Lib/Word_Lemmas_32.thy

thys/Word_Lib/Word_Lemmas_64.thy

thys/Word_Lib/Word_Lib_Sumo.thy

thys/Word_Lib/Word_Setup_32.thy

thys/Word_Lib/Word_Setup_64.thy

thys/Word_Lib/Word_Syntax.thy

dedicated integration theory for word8/16/32/64
c8d4f20a1071
Actions