Diffusion Isabelle 9a1796acd0a4

merged
9a1796acd0a4
Actions

Description

merged

Details

Provenance

nipkow

Authored on

Parents

rISABELLEd4af818e0880: Backed out changeset fe8d0f4da0e6
rISABELLE62b0577123a5: merged

Branches

Unknown

Tags

Unknown

Event Timeline

nipkow committed rISABELLE9a1796acd0a4: merged.Aug 18 2021, 12:33 PM

Merged Changes

This commit merges a very large number of changes. Only the first 50 are shown.

ea10e06adede more Isabelle/Haskell operations;
Author
makarius
Browse Repository
No Builds
No Audits
6109a9105a7a more Isabelle/Haskell operations;
Author
makarius
Browse Repository
No Builds
No Audits
92e74f9305a4 more Isabelle/Haskell operations;
Author
makarius
Browse Repository
No Builds
No Audits
2508ea6a9a11 more Isabelle/Haskell operations;
Author
makarius
Browse Repository
No Builds
No Audits
7652f8d29d10 clarified signature;
Author
makarius
Browse Repository
No Builds
No Audits
af81e4a307be clarified signature;
Author
makarius
Browse Repository
No Builds
No Audits
72bb7e9143f7 minor performance tuning;
Author
makarius
Browse Repository
No Builds
No Audits
4ae14c2e7cdd tuned;
Author
makarius
Browse Repository
No Builds
No Audits
5d40a4f66fdd tuned;
Author
makarius
Browse Repository
No Builds
No Audits
54e096758b63 tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
5f81ebfb551e tuned comments;
Author
makarius
Browse Repository
No Builds
No Audits
a8b032dede5c treat Symbol.eof as in ML (but: presently unused);
Author
makarius
Browse Repository
No Builds
No Audits
b70714530045 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
53e28c438f96 minor performance tuning;
Author
makarius
Browse Repository
No Builds
No Audits
a3b0fc510705 clarified signature;
Author
makarius
Browse Repository
No Builds
No Audits
8d03d548df1c proper Isabelle symbol positions;
Author
makarius
Browse Repository
No Builds
No Audits
c576a4e2ffbc more Haskell operations;
Author
makarius
Browse Repository
No Builds
No Audits
a9e79c3645c4 clarified signature;
Author
makarius
Browse Repository
No Builds
No Audits
09d4175f473e tuned;
Author
makarius
Browse Repository
No Builds
No Audits
43fe7388458f tuned;
Author
makarius
Browse Repository
No Builds
No Audits
f0b2136e2204 tuned signature: prefer existing Haskell operations;
Author
makarius
Browse Repository
No Builds
No Audits
25c672c32467 more Haskell operations;
Author
makarius
Browse Repository
No Builds
No Audits
ff3dbb2be924 tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
86163ea20e77 tuned comments;
Author
makarius
Browse Repository
No Builds
No Audits
7b93dc3f2b34 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
afe3c8ae1624 consolidation of rules for bit operations
Author
florian.haftmann
Browse Repository
No Builds
No Audits
304f22435bc7 fixed $ite syntax in TPTP TFX generation
Author
desharna
Browse Repository
No Builds
No Audits
3f371ba2b4fc more Haskell operations;
Author
makarius
Browse Repository
No Builds
No Audits
b5eba4717648 merged
Author
makarius
Browse Repository
No Builds
No Audits
c6bce3633c53 revert 0faa68dedce5: very slow;
Author
makarius
Browse Repository
No Builds
No Audits
1cb0ad6f9a2d tuned;
Author
makarius
Browse Repository
No Builds
No Audits
8e2355ddce1b add/rename some theorems about Map(pings)
Author
lukasstevens
Browse Repository
No Builds
No Audits
ecf80e37ed1a support configuration options "show_results";
Author
makarius
Browse Repository
No Builds
No Audits
0faa68dedce5 consolidate_body more thoroughly, e.g. for reduced ML_Heap.obj_size;
Author
makarius
Browse Repository
No Builds
No Audits
62b0577123a5 merged
Author
desharna
Browse Repository
No Builds
No Audits
46f66e821f5c fixed $ite syntax in TPTP THX generation
Author
desharna
Browse Repository
No Builds
No Audits
069f6b2c5a07 tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
c3b3517ef4ba more scalable data structures;
Author
makarius
Browse Repository
No Builds
No Audits
de12016ffefb more scalable data structures;
Author
makarius
Browse Repository
No Builds
No Audits
9e73600ec75d more scalable data structures;
Author
makarius
Browse Repository
No Builds
No Audits
a97d5356f1d9 proper position information for Context.theory_data_size;
Author
makarius
Browse Repository
No Builds
No Audits
d030b988d470 provide bash_process server for Isabelle/ML and other external programs;
Author
makarius
Browse Repository
No Builds
No Audits
dd1639961016 clarified signature;
Author
makarius
Browse Repository
No Builds
No Audits
608f8ae89cac clarified signature;
Author
makarius
Browse Repository
No Builds
No Audits
f9f6a31cc99c proper prover_options for batch-build;
Author
makarius
Browse Repository
No Builds
No Audits
8d20b1cf0d5d clarified signature;
Author
makarius
Browse Repository
No Builds
No Audits
0f051404f487 clarified signature: more options for bash_process;
Author
makarius
Browse Repository
No Builds
No Audits
bba35ad317ab tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
8a5e02ef975c clarified signature;
Author
makarius
Browse Repository
No Builds
No Audits
3314559ef095 clarified signature;
Author
makarius
Browse Repository
No Builds
No Audits

Changes (14)

Path

Size

rISABELLE9a1796acd0a4

View Options

src/Tools/ROOT

View Options

src/Tools/Spec_Check/Examples.thy

View Options

src/Tools/Spec_Check/README

View Options

src/Tools/Spec_Check/Spec_Check.thy

View Options

src/Tools/Spec_Check/base_generator.ML

View Options

src/Tools/Spec_Check/gen_construction.ML

View Options

src/Tools/Spec_Check/generator.ML

View Options

src/Tools/Spec_Check/output_style.ML

View Options

src/Tools/Spec_Check/property.ML

View Options

src/Tools/Spec_Check/random.ML

View Options

src/Tools/Spec_Check/spec_check.ML

merged9a1796acd0a4Actions

Description

Details

Event Timeline

Merged Changes

Changes (14)

rISABELLE9a1796acd0a4

src/Tools/ROOT

src/Tools/Spec_Check/Examples.thy

src/Tools/Spec_Check/README

src/Tools/Spec_Check/Spec_Check.thy

src/Tools/Spec_Check/base_generator.ML

src/Tools/Spec_Check/gen_construction.ML

src/Tools/Spec_Check/generator.ML

src/Tools/Spec_Check/output_style.ML

src/Tools/Spec_Check/property.ML

src/Tools/Spec_Check/random.ML

src/Tools/Spec_Check/spec_check.ML

merged
9a1796acd0a4
Actions