fix reconstruction of Alethe's and_pos rule
157de27b0863
Actions

Description

fix reconstruction of Alethe's and_pos rule

Details

Provenance

Authored on

Parents

Branches

Unknown

Tags

Unknown

Changes (5)

Path

Size

src/

HOL/

SMT_Examples/

Tools/

SMT/

rISABELLE157de27b0863

src/HOL/SMT.thy

src/HOL/SMT_Examples/SMT_Examples_Verit.certs

src/HOL/SMT_Examples/SMT_Examples_Verit.thy

src/HOL/Tools/SMT/lethe_replay_methods.ML

src/HOL/Tools/SMT/smt_replay_arith.ML

fix reconstruction of Alethe's and_pos rule157de27b0863Actions

Description

Details

Changes (5)

rISABELLE157de27b0863

src/HOL/SMT.thy

src/HOL/SMT_Examples/SMT_Examples_Verit.certs

src/HOL/SMT_Examples/SMT_Examples_Verit.thy

src/HOL/Tools/SMT/lethe_replay_methods.ML

src/HOL/Tools/SMT/smt_replay_arith.ML

fix reconstruction of Alethe's and_pos rule
157de27b0863
Actions