Diffusion Isabelle fa247805669d

merge in backouts
fa247805669d
Actions

Tags

None

Subscribers

None

Description

merge in backouts

Details

Provenance

Authored on

Parents

rISABELLE6470353996f5: Backed out changeset 1fde0e4fd791
rISABELLEf02c8a45c4c1: Backed out changeset bafdc56654cf

Branches

Unknown

Tags

Unknown

Event Timeline

nipkow committed rISABELLEfa247805669d: merge in backouts.Feb 20 2023, 1:59 PM

Merged Changes

f02c8a45c4c1 Backed out changeset bafdc56654cf
Author
nipkow
Browse Repository
No Builds
No Audits
0794ec39a4e0 backout rev 334015f9098e (for Main_Doc.thy only)
Author
nipkow
Browse Repository
No Builds
No Audits
aea11797247b merged
Author
paulson
Browse Repository
No Builds
No Audits
3c4aca1266eb Simplifying more proofs
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
632a92fcb673 merged
Author
makarius
Browse Repository
No Builds
No Audits
c6d724692603 proper Nodes.init (amending 9b35c1171d9a);
Author
makarius
Browse Repository
No Builds
No Audits
57467fdd507d unused;
Author
makarius
Browse Repository
No Builds
No Audits
026e1bb04a05 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
39c7d79ace34 clarified signature defaults;
Author
makarius
Browse Repository
No Builds
No Audits
226a880d0423 clarified types: support a variety of Build_Job instances;
Author
makarius
Browse Repository
No Builds
No Audits
eeaa2872320b clarified signature: more explicit synchronized operations;
Author
makarius
Browse Repository
No Builds
No Audits
ab13ac27c74a clarified signature: more explicit synchronized operations;
Author
makarius
Browse Repository
No Builds
No Audits
3f2b1419f598 clarified modules (again);
Author
makarius
Browse Repository
No Builds
No Audits
4f4a0c9d2d1a clarified signature: more explicit synchronized operations;
Author
makarius
Browse Repository
No Builds
No Audits
9cb8fb31e245 clarified signature: more explicit synchronized operations;
Author
makarius
Browse Repository
No Builds
No Audits
f7e413e8d269 more robust: first register job, then start job;
Author
makarius
Browse Repository
No Builds
No Audits
12fd873af77c clarified signature: proper scope of synchronized operation;
Author
makarius
Browse Repository
No Builds
No Audits
c7d893278aec proper synchronized access to mutable state, to support concurrency eventually;
Author
makarius
Browse Repository
No Builds
No Audits
e9f1fcb9b358 tuned signature: explicit marker for mutable global state;
Author
makarius
Browse Repository
No Builds
No Audits
d060545f01a2 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
6435b0fd48b5 more robust;
Author
makarius
Browse Repository
No Builds
No Audits
f04672649483 clarified signature;
Author
makarius
Browse Repository
No Builds
No Audits
2bf321758333 clarified modules;
Author
makarius
Browse Repository
No Builds
No Audits
98dab34ed72d merged
Author
paulson
Browse Repository
No Builds
No Audits
3fc7c85fdbb5 Tidied some really messy proofs
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
3a2670c37e5c added lemmas asymp_not_liftable_to_multpHO and asymp_multpHO
Author
desharna
Browse Repository
No Builds
No Audits
8543e6b10a56 Simplified a few proofs
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
c16d423c9cb1 Moved up a theorem
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
e20f5b9ad776 Limit properties for complex exponential
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
c6b50597abbc More of Eberl's contributions: memomorphic functions
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
29032b496f2e merged
Author
paulson
Browse Repository
No Builds
No Audits
386b1b33785c New material due to Eberl on Formal Laurent Series
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
05ad117ee3fb merged
Author
paulson
Browse Repository
No Builds
No Audits
f82317de6f28 A bit more tidying and some new material
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits

Changes (19)

Path

Size

src/

Doc/

Sledgehammer/

document/

HOL/

Data_Structures/

Tools/

ATP/

atp_proof_reconstruct.ML

Meson/

meson_clausify.ML

SMT/

Sledgehammer/

sledgehammer.ML

sledgehammer_atp_systems.ML

sledgehammer_commands.ML

sledgehammer_fact.ML

sledgehammer_mash.ML

sledgehammer_prover.ML

sledgehammer_prover_atp.ML

sledgehammer_prover_minimize.ML

sledgehammer_prover_smt.ML

sledgehammer_tactics.ML

rISABELLEfa247805669d

NEWS

Loading...

src/Doc/Sledgehammer/document/root.tex

Loading...

src/HOL/Data_Structures/RBT_Map.thy

Loading...

src/HOL/Metis.thy

Loading...

src/HOL/Tools/ATP/atp_proof.ML

Loading...

src/HOL/Tools/ATP/atp_proof_reconstruct.ML

Loading...

src/HOL/Tools/Meson/meson_clausify.ML

Loading...

src/HOL/Tools/SMT/smt_solver.ML

Loading...

src/HOL/Tools/SMT/smt_systems.ML

Loading...

src/HOL/Tools/Sledgehammer/sledgehammer.ML

Loading...

src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML

Loading...

src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML

Loading...

src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML

Loading...

src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML

Loading...

src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML

Loading...

src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML

Loading...

src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML

Loading...

src/HOL/Tools/Sledgehammer/sledgehammer_prover_smt.ML

Loading...

src/HOL/Tools/Sledgehammer/sledgehammer_tactics.ML

Loading...