Diffusion afp-devel ec1c704f4022

tuned proofs: avoid z3 to make it work on arm64-linux;
ec1c704f4022
Actions

Tags

None

Subscribers

None

Description

tuned proofs: avoid z3 to make it work on arm64-linux;

Details

Provenance

Authored on

Parents

rAFP09e32ec351bb: v1.0.1.0

Branches

Unknown

Tags

Unknown

Event Timeline

makarius committed rAFPec1c704f4022: tuned proofs: avoid z3 to make it work on arm64-linux;.Wed, Apr 10, 9:34 PM

Changes (16)

Path

Size

thys/

Cook_Levin/

Aux_TM_Reducing.thy

Combinations.thy

Lists_Lists.thy

Oblivious_2_Tape.thy

Oblivious_Polynomial.thy

Satisfiability.thy

Two_Four_Symbols.thy

rAFPec1c704f4022

thys/Cook_Levin/Arithmetic.thy

Loading...

thys/Cook_Levin/Aux_TM_Reducing.thy

Loading...

thys/Cook_Levin/Basics.thy

Loading...

thys/Cook_Levin/Combinations.thy

Loading...

thys/Cook_Levin/Composing.thy

Loading...

thys/Cook_Levin/Elementary.thy

Loading...

thys/Cook_Levin/Lists_Lists.thy

Loading...

thys/Cook_Levin/NP.thy

Loading...

thys/Cook_Levin/Oblivious.thy

Loading...

thys/Cook_Levin/Oblivious_2_Tape.thy

Loading...

thys/Cook_Levin/Oblivious_Polynomial.thy

Loading...

thys/Cook_Levin/Reducing.thy

Loading...

thys/Cook_Levin/Sat_TM_CNF.thy

Loading...

thys/Cook_Levin/Satisfiability.thy

Loading...

thys/Cook_Levin/Symbol_Ops.thy

Loading...

thys/Cook_Levin/Two_Four_Symbols.thy

Loading...