Diffusion afp-devel d6be5fd1a75a

factored out operations
d6be5fd1a75a
Actions

Tags

None

Subscribers

None

Description

factored out operations

Details

Provenance

florian.haftmann

Authored on

Parents

rAFP3b3d09186d48: more collecting and grouping of lemmas

Branches

Unknown

Tags

Unknown

Event Timeline

florian.haftmann committed rAFPd6be5fd1a75a: factored out operations.Nov 19 2020, 4:22 PM

Changes (17)

Path

Size

Native_Word/

Code_Target_Word_Base.thy

More_Divides.thy

More_Word_Operations.thy

Next_and_Prev.thy

Signed_Division_Word.thy

Traditional_Infix_Syntax.thy

Word_Lemmas.thy

Word_Lib_Sumo.thy

rAFPd6be5fd1a75a

thys/Native_Word/Code_Target_Word_Base.thy

Loading...

thys/Word_Lib/Aligned.thy

Loading...

thys/Word_Lib/Examples.thy

Loading...

thys/Word_Lib/Guide.thy

Loading...

thys/Word_Lib/More_Divides.thy

Loading...

thys/Word_Lib/More_Misc.thy

Loading...

thys/Word_Lib/More_Word.thy

Loading...

thys/Word_Lib/More_Word_Operations.thy

Loading...

thys/Word_Lib/Next_and_Prev.thy

Loading...

thys/Word_Lib/Signed_Division_Word.thy

Loading...

thys/Word_Lib/Traditional_Infix_Syntax.thy

Loading...

thys/Word_Lib/Word_EqI.thy

Loading...

thys/Word_Lib/Word_Lemmas.thy

Loading...

thys/Word_Lib/Word_Lib.thy

Loading...

thys/Word_Lib/Word_Lib_Sumo.thy

Loading...