Avoid explicit operation when not necessary.
95b886c17e9a
Actions

Description

Avoid explicit operation when not necessary.

Details

Provenance

Authored on

Parents

Branches

Unknown

Tags

Unknown

Changes (5)

Path

Size

thys/

Native_Word/

rAFP95b886c17e9a

thys/Native_Word/Code_Target_Word_Base.thy

thys/Native_Word/Uint.thy

thys/Native_Word/Uint32.thy

thys/Native_Word/Uint64.thy

thys/Native_Word/Word_Type_Copies.thy

Avoid explicit operation when not necessary.95b886c17e9aActions

Description

Details

Changes (5)

rAFP95b886c17e9a

thys/Native_Word/Code_Target_Word_Base.thy

thys/Native_Word/Uint.thy

thys/Native_Word/Uint32.thy

thys/Native_Word/Uint64.thy

thys/Native_Word/Word_Type_Copies.thy

Avoid explicit operation when not necessary.
95b886c17e9a
Actions