Diffusion afp-devel c42c2c2447c2

avoid overaggressive contraction of conversions
c42c2c2447c2
Actions

Tags

None

Subscribers

None

Description

avoid overaggressive contraction of conversions

Details

Provenance

florian.haftmann

Authored on

Parents

rAFP721d0f625e02: slightly more prominence for proof tools; more examples

Branches

Unknown

Tags

Unknown

Event Timeline

florian.haftmann committed rAFPc42c2c2447c2: avoid overaggressive contraction of conversions.Oct 10 2021, 4:45 PM

Changes (16)

Path

Size

thys/

Berlekamp_Zassenhaus/

Finite_Field_Record_Based.thy

CAVA_LTL_Modelchecker/

SM/

RefPoint/

Complx/

ex/

IEEE_Floating_Point/

Conversion_IEEE_Float.thy

Iptables_Semantics/

Common/

Native_Word/

Code_Target_Word_Base.thy

PAC_Checker/

PAC_Checker_Relation.thy

SPARCv8/

SparcModel_MMU/

Sparc_Properties.thy

Word_Lib/

More_Word_Operations.thy

Word_Lemmas.thy

rAFPc42c2c2447c2

thys/Berlekamp_Zassenhaus/Finite_Field_Record_Based.thy

Loading...

thys/CAVA_LTL_Modelchecker/SM/RefPoint/SM_State.thy

Loading...

thys/Complx/ex/SumArr.thy

Loading...

thys/IEEE_Floating_Point/Conversion_IEEE_Float.thy

Loading...

thys/Iptables_Semantics/Common/Word_Upto.thy

Loading...

thys/Native_Word/Code_Target_Word_Base.thy

Loading...

thys/PAC_Checker/PAC_Checker_Relation.thy

Loading...

thys/SPARCv8/SparcModel_MMU/Sparc_Properties.thy

Loading...

thys/Word_Lib/Aligned.thy

Loading...

thys/Word_Lib/More_Word.thy

Loading...

thys/Word_Lib/More_Word_Operations.thy

Loading...

thys/Word_Lib/Rsplit.thy

Loading...

thys/Word_Lib/Word_32.thy

Loading...

thys/Word_Lib/Word_64.thy

Loading...

thys/Word_Lib/Word_8.thy

Loading...

thys/Word_Lib/Word_Lemmas.thy

Loading...