Diffusion Isabelle 0d065af1a99c

merged
0d065af1a99c
Actions

Tags

None

Subscribers

None

Description

merged

Details

Provenance

Authored on

Parents

rISABELLEaf34c689bfda: merged
rISABELLE3c57995c255c: allow higher-order unification of open terms (reviewed by Larry Paulson)

Branches

Unknown

Tags

Unknown

Event Timeline

paulson committed rISABELLE0d065af1a99c: merged.Sat, Sep 9, 6:18 PM

Merged Changes

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

3c57995c255c allow higher-order unification of open terms (reviewed by Larry Paulson)
Author
kappelmann
Browse Repository
No Builds
No Audits
d17fcfd075c3 merged
Author
makarius
Browse Repository
No Builds
No Audits
47d0c333d155 clarified signature: retain original Poly/ML names Thread.Thread, Thread.Mutex…
Author
makarius
Browse Repository
No Builds
No Audits
d46006355819 add ML_system_pp for type Isabelle_Thread.T;
Author
makarius
Browse Repository
No Builds
No Audits
852ec09aef13 more explicit type Isabelle_Thread.T;
Author
makarius
Browse Repository
No Builds
No Audits
27380538d632 discontinue somewhat pointless thread tracing/debugging: without PIDE command…
Author
makarius
Browse Repository
No Builds
No Audits
fff610f1a6f4 tuned whitespace;
Author
makarius
Browse Repository
No Builds
No Audits
de8081bc85a0 tuned Sledgehammer messages
Author
blanchette
Browse Repository
No Builds
No Audits
a7bcd2af7190 respect timeout better
Author
blanchette
Browse Repository
No Builds
No Audits
d5a1d64a563d merged
Author
makarius
Browse Repository
No Builds
No Audits
4f2215cfc3e0 Added tag Isabelle2023-RC5 for changeset ffa417b5c913
Author
makarius
Browse Repository
No Builds
No Audits
ffa417b5c913 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
5ee978b3c009 tuned messages;
Author
makarius
Browse Repository
No Builds
No Audits
ca56952b7322 proper stop of build_process shutdown, despite errors on workers;
Author
makarius
Browse Repository
No Builds
No Audits
28a2c55648d5 prefer quiet mode: potentially more robust ssh connection, e.g. when master…
Author
makarius
Browse Repository
No Builds
No Audits
9a5d86549719 support "isabelle build_worker -q";
Author
makarius
Browse Repository
No Builds
No Audits
163c392675dc support "isabelle build_process -r -f";
Author
makarius
Browse Repository
No Builds
No Audits
26a02b042fe0 clarified signature;
Author
makarius
Browse Repository
No Builds
No Audits
0beb46a96cf3 clarified output;
Author
makarius
Browse Repository
No Builds
No Audits
37a0c953649d clarified signature;
Author
makarius
Browse Repository
No Builds
No Audits
e3d7793545df clarified signature: removed ununsed option;
Author
makarius
Browse Repository
No Builds
No Audits
0649be5c3036 tuned message;
Author
makarius
Browse Repository
No Builds
No Audits
93756069b867 updated to naproche-20230902: add examples/100_theorems.ftl.tex and some more…
Author
makarius
Browse Repository
No Builds
No Audits
569135d7352a more robust access to output file of external smt, notably for Windows 11…
Author
makarius
Browse Repository
No Builds
No Audits
adf227c06812 more robust $ISABELLE_TMP_PREFIX on windows: avoid location within Cygwin root…
Author
makarius
Browse Repository
No Builds
No Audits
fa18208fd7bd more robust $TMPDIR on windows, e.g. for repository snapshot: do not depend on…
Author
makarius
Browse Repository
No Builds
No Audits
f926602640fe more portable: it really is the Cygwin $HOME not the Windows $USER_HOME;
Author
makarius
Browse Repository
No Builds
No Audits
6aa964f52395 more accurate documentation of record field update, following changes in…
Author
makarius
Browse Repository
No Builds
No Audits
8d7394e533f8 tuned whitespace;
Author
makarius
Browse Repository
No Builds
No Audits
b96b73a79da3 more robust: "hostname" command might be absent, notably on Arch Linux (and…
Author
makarius
Browse Repository
No Builds
No Audits
c42f316f0a01 tuned NEWS;
Author
makarius
Browse Repository
No Builds
No Audits
931f819728df NEWS;
Author
makarius
Browse Repository
No Builds
No Audits
6a9c5ea774e8 update to "scalac -source 3.3" (from 3.1);
Author
makarius
Browse Repository
No Builds
No Audits
193a24f78b00 proper pattern (amending ff86f10e54cd);
Author
makarius
Browse Repository
No Builds
No Audits
209607465a90 discontinue odd AFP partitioning: let Build_Cluster / Build_Engine do the job;
Author
makarius
Browse Repository
No Builds
No Audits
2c3a05b297f4 discontinue special treatment of AFP: "isabelle dump" has been superseded by…
Author
makarius
Browse Repository
No Builds
No Audits
9acd819db33a clarified signature: prefer enum types;
Author
makarius
Browse Repository
No Builds
No Audits
abdf38ee314a proper type, following Bus.event;
Author
makarius
Browse Repository
No Builds
No Audits
4da5cdaa4dcd clarified signature;
Author
makarius
Browse Repository
No Builds
No Audits
60561d28569b clarified signature: prefer enum types;
Author
makarius
Browse Repository
No Builds
No Audits
f7df1a444dbb clarified signature: prefer enum types;
Author
makarius
Browse Repository
No Builds
No Audits
7b80cc4701c2 clarified signature: prefer enum types;
Author
makarius
Browse Repository
No Builds
No Audits
fd1fec53665b clarified signature: prefer enum types;
Author
makarius
Browse Repository
No Builds
No Audits
67492b2a3a62 clarified signature: prefer enum types;
Author
makarius
Browse Repository
No Builds
No Audits
0e01c3b55b63 clarified signature: prefer enum types;
Author
makarius
Browse Repository
No Builds
No Audits
3f3add5eef91 tuned indentation;
Author
makarius
Browse Repository
No Builds
No Audits
7bfac764a715 clarified signature: prefer enum types;
Author
makarius
Browse Repository
No Builds
No Audits
0bbbf8e26708 clarified signature: prefer enum types;
Author
makarius
Browse Repository
No Builds
No Audits
9ccd5e8737cb clarified signature: prefer enum types;
Author
makarius
Browse Repository
No Builds
No Audits
2401b5d9cee9 clarified signature: prefer enum types;
Author
makarius
Browse Repository
No Builds
No Audits

Changes (4)

Path

Size

src/

HOL/

Data_Structures/

Array_Braun.thy

Brother12_Set.thy

Tries_Binary.thy

rISABELLE0d065af1a99c

src/HOL/Data_Structures/Array_Braun.thy

Loading...

src/HOL/Data_Structures/Brother12_Set.thy

Loading...

src/HOL/Data_Structures/Sorting.thy

Loading...

src/HOL/Data_Structures/Tries_Binary.thy

Loading...