HomeIsabelle/Phabricator
Diffusion Isabelle 1e2a9d2251b0

remove duplicate parsing for alethe; fix skolemization;
1e2a9d2251b0
Actions

Description

remove duplicate parsing for alethe; fix skolemization;

Details

Provenance
mathias.fleuryAuthored on
Parents
rISABELLE5305c65dcbb2: Gauss numbers
Branches
Unknown
Tags
Unknown

Changes (16)

PathSize
SMT_Examples/
verit_strategies.ML
verit_proof.ML
Sledgehammer/

rISABELLE1e2a9d2251b0

View Options

src/HOL/SMT.thy

Loading...
View Options

src/HOL/SMT_Examples/SMT_Examples_Verit.certs

Loading...
View Options

src/HOL/SMT_Examples/SMT_Examples_Verit.thy

Loading...
View Options

src/HOL/Tools/SMT/lethe_proof.ML

Loading...
View Options

src/HOL/Tools/SMT/lethe_replay_methods.ML

Loading...
View Options

src/HOL/Tools/SMT/smt_systems.ML

Loading...
View Options

src/HOL/Tools/SMT/verit_proof.ML

Loading...
View Options

src/HOL/Tools/SMT/verit_replay.ML

Loading...
View Options

src/HOL/Tools/SMT/verit_strategies.ML

Loading...
View Options

src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

Loading...
View Options

src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML

Loading...
View Options

src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML

Loading...