separated non-computable instance of bit comprehension from computable one
01df7496c94e
Actions

Description

separated non-computable instance of bit comprehension from computable one

Details

Provenance

Authored on

Parents

Branches

Unknown

Tags

Unknown

Changes (7)

Path

Size

Native_Word/

rAFP01df7496c94e

thys/Native_Word/Code_Target_Integer_Bit.thy

thys/Word_Lib/Bit_Comprehension.thy

thys/Word_Lib/Bit_Comprehension_Int.thy

thys/Word_Lib/Guide.thy

thys/Word_Lib/Word_Lib_Sumo.thy

separated non-computable instance of bit comprehension from computable one01df7496c94eActions

Description

Details

Changes (7)

rAFP01df7496c94e

thys/Native_Word/Code_Target_Integer_Bit.thy

thys/Word_Lib/Bit_Comprehension.thy

thys/Word_Lib/Bit_Comprehension_Int.thy

thys/Word_Lib/Guide.thy

thys/Word_Lib/Word_Lib_Sumo.thy

separated non-computable instance of bit comprehension from computable one
01df7496c94e
Actions