Diffusion afp-devel 5456b058dbbf

tuned structure formally
5456b058dbbf
Actions

Description

tuned structure formally

Details

Provenance

florian.haftmann

Authored on

Parents

rAFP88b8151dff90: updated to new Leftist_Heap

Branches

Unknown

Tags

Unknown

Event Timeline

florian.haftmann committed rAFP5456b058dbbf: tuned structure formally.Nov 4 2020, 8:39 AM

Changes (56)

Path

Size

thys

Berlekamp_Zassenhaus/

Poly_Mod.thy

CAVA_LTL_Modelchecker/

SM/

RefPoint/

SM_State.thy

CakeML/

generated/

IP_Addresses/

Interval_Arithmetic_Word32/

Interval_Word32.thy

JinjaThreads/

Common/

BinOp.thy

Native_Word/

Code_Symbolic_Bits_Int.thy

Code_Target_Word_Base.thy

SPARCv8/

SparcModel_MMU/

Bit_Comprehension.thy

Bits_Int.thy

Bitwise.thy

	Enumeration_Word.thy
	Word_Enum.thy

Examples.thy

	Generic_set_bit.thy
	Misc_set_bit.thy

Guide.thy

HOL_Lemmas.thy

	Least_significant_bit.thy
	Misc_lsb.thy

	More_Arithmetic.thy
	Misc_Arithmetic.thy

	More_List.thy
	Misc_Auxiliary.thy

	More_Misc.thy
	HOL_Lemmas.thy

More_Word.thy

	Most_significant_bit.thy
	Misc_msb.thy

	Next_and_Prev.thy
	Word_Next.thy

Norm_Words.thy

ROOT

Reversed_Bit_Lists.thy

Rsplit.thy

	Traditional_Infix_Syntax.thy
	Traditional_Syntax.thy

Traditional_Syntax.thy

	Type_Syntax.thy
	Word_Type_Syntax.thy

	Typedef_Morphisms.thy
	Misc_Typedef.thy

	Word_Lib_Sumo.thy
	More_Word.thy

rAFP5456b058dbbf

View Options

thys/Berlekamp_Zassenhaus/Poly_Mod.thy

View Options

thys/CAVA_LTL_Modelchecker/SM/RefPoint/SM_State.thy

View Options

thys/CakeML/generated/Lem_machine_word.thy

View Options

thys/IP_Addresses/IPv4.thy

View Options

thys/IP_Addresses/NumberWang_IPv6.thy

View Options

thys/IP_Addresses/WordInterval.thy

View Options

thys/Interval_Arithmetic_Word32/Interval_Word32.thy

View Options

thys/JinjaThreads/Common/BinOp.thy

View Options

thys/Native_Word/Code_Symbolic_Bits_Int.thy

View Options

thys/Native_Word/Code_Target_Word_Base.thy

View Options

thys/SPARCv8/SparcModel_MMU/RegistersOps.thy

View Options

thys/SPARCv8/SparcModel_MMU/Sparc_Types.thy

View Options

thys/Word_Lib/Aligned.thy

View Options

thys/Word_Lib/Ancient_Numeral.thy

View Options

thys/Word_Lib/Bit_Comprehension.thy

View Options

thys/Word_Lib/Bits_Int.thy

View Options

thys/Word_Lib/Bitwise.thy

View Options

thys/Word_Lib/Enumeration_Word.thy

View Options

thys/Word_Lib/Examples.thy

View Options

thys/Word_Lib/Generic_set_bit.thy

View Options

thys/Word_Lib/Guide.thy

View Options

thys/Word_Lib/HOL_Lemmas.thy

View Options

thys/Word_Lib/Least_significant_bit.thy

View Options

thys/Word_Lib/Misc_Arithmetic.thy

View Options

thys/Word_Lib/Misc_Auxiliary.thy

View Options

thys/Word_Lib/Misc_Typedef.thy

View Options

thys/Word_Lib/Misc_lsb.thy

View Options

thys/Word_Lib/Misc_msb.thy

View Options

thys/Word_Lib/Misc_set_bit.thy

View Options

thys/Word_Lib/More_Arithmetic.thy

View Options

thys/Word_Lib/More_List.thy

View Options

thys/Word_Lib/More_Misc.thy

View Options

thys/Word_Lib/More_Word.thy

View Options

thys/Word_Lib/Most_significant_bit.thy

View Options

thys/Word_Lib/Next_and_Prev.thy

View Options

thys/Word_Lib/Norm_Words.thy

View Options

thys/Word_Lib/ROOT

View Options

thys/Word_Lib/Reversed_Bit_Lists.thy

View Options

thys/Word_Lib/Rsplit.thy

View Options

thys/Word_Lib/Traditional_Infix_Syntax.thy

View Options

thys/Word_Lib/Traditional_Syntax.thy

View Options

thys/Word_Lib/Type_Syntax.thy

View Options

thys/Word_Lib/Typedef_Morphisms.thy

View Options

thys/Word_Lib/Word_Enum.thy

View Options

thys/Word_Lib/Word_EqI.thy

View Options

thys/Word_Lib/Word_Examples.thy

View Options

thys/Word_Lib/Word_Lemmas.thy

View Options

thys/Word_Lib/Word_Lib.thy

View Options

thys/Word_Lib/Word_Lib_Sumo.thy

View Options

thys/Word_Lib/Word_Next.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_Type_Syntax.thy

View Options

thys/Word_Lib/Word_rsplit.thy

tuned structure formally5456b058dbbfActions

Description

Details

Event Timeline

Changes (56)

rAFP5456b058dbbf

thys/Berlekamp_Zassenhaus/Poly_Mod.thy

thys/CAVA_LTL_Modelchecker/SM/RefPoint/SM_State.thy

thys/CakeML/generated/Lem_machine_word.thy

thys/IP_Addresses/IPv4.thy

thys/IP_Addresses/NumberWang_IPv6.thy

thys/IP_Addresses/WordInterval.thy

thys/Interval_Arithmetic_Word32/Interval_Word32.thy

thys/JinjaThreads/Common/BinOp.thy

thys/Native_Word/Code_Symbolic_Bits_Int.thy

thys/Native_Word/Code_Target_Word_Base.thy

thys/SPARCv8/SparcModel_MMU/RegistersOps.thy

thys/SPARCv8/SparcModel_MMU/Sparc_Types.thy

thys/Word_Lib/Aligned.thy

thys/Word_Lib/Ancient_Numeral.thy

thys/Word_Lib/Bit_Comprehension.thy

thys/Word_Lib/Bits_Int.thy

thys/Word_Lib/Bitwise.thy

thys/Word_Lib/Enumeration_Word.thy

thys/Word_Lib/Examples.thy

thys/Word_Lib/Generic_set_bit.thy

thys/Word_Lib/Guide.thy

thys/Word_Lib/HOL_Lemmas.thy

thys/Word_Lib/Least_significant_bit.thy

thys/Word_Lib/Misc_Arithmetic.thy

thys/Word_Lib/Misc_Auxiliary.thy

thys/Word_Lib/Misc_Typedef.thy

thys/Word_Lib/Misc_lsb.thy

thys/Word_Lib/Misc_msb.thy

thys/Word_Lib/Misc_set_bit.thy

thys/Word_Lib/More_Arithmetic.thy

thys/Word_Lib/More_List.thy

thys/Word_Lib/More_Misc.thy

thys/Word_Lib/More_Word.thy

thys/Word_Lib/Most_significant_bit.thy

thys/Word_Lib/Next_and_Prev.thy

thys/Word_Lib/Norm_Words.thy

thys/Word_Lib/ROOT

thys/Word_Lib/Reversed_Bit_Lists.thy

thys/Word_Lib/Rsplit.thy

thys/Word_Lib/Traditional_Infix_Syntax.thy

thys/Word_Lib/Traditional_Syntax.thy

thys/Word_Lib/Type_Syntax.thy

thys/Word_Lib/Typedef_Morphisms.thy

thys/Word_Lib/Word_Enum.thy

thys/Word_Lib/Word_EqI.thy

thys/Word_Lib/Word_Examples.thy

thys/Word_Lib/Word_Lemmas.thy

thys/Word_Lib/Word_Lib.thy

thys/Word_Lib/Word_Lib_Sumo.thy

thys/Word_Lib/Word_Next.thy

thys/Word_Lib/Word_Setup_32.thy

thys/Word_Lib/Word_Setup_64.thy

thys/Word_Lib/Word_Type_Syntax.thy

thys/Word_Lib/Word_rsplit.thy

tuned structure formally
5456b058dbbf
Actions