Diffusion Isabelle 8641f16abc7a

merged
8641f16abc7a
Actions

Tags

None

Subscribers

None

Description

merged

Details

Provenance

Authored on

Parents

rISABELLE561d501598f2: update naproche component;
rISABELLE045729b42c5d: merged

Branches

Unknown

Tags

Unknown

Event Timeline

makarius committed rISABELLE8641f16abc7a: merged.Oct 18 2022, 2:15 PM

Merged Changes

561d501598f2 update naproche component;
Author
makarius
Browse Repository
No Builds
No Audits
c56997fab437 Added tag Isabelle2022-RC4 for changeset 8b4108f41c77
Author
makarius
Browse Repository
No Builds
No Audits
8b4108f41c77 rebuild with proper Isabelle version;
Author
makarius
Browse Repository
No Builds
No Audits
bc4f902d2b0d removed junk;
Author
makarius
Browse Repository
No Builds
No Audits
0749f4d4b5be more robust, e.g. for "isabelle dump";
Author
makarius
Browse Repository
No Builds
No Audits
cdef2c8beccf more robust, e.g. for "isabelle dump";
Author
makarius
Browse Repository
No Builds
No Audits
79ef5d0fff00 more robust, e.g. for "isabelle dump";
Author
makarius
Browse Repository
No Builds
No Audits
f70b015e4ac1 allow spaces in SCALA_HOME directory name;
Author
makarius
Browse Repository
No Builds
No Audits
a39fa81929d4 avoid spurious error messages, e.g. when scala is missing;
Author
makarius
Browse Repository
No Builds
No Audits
14cf5a50c1e9 more NEWS;
Author
makarius
Browse Repository
No Builds
No Audits
6108b1751c1b tuned, following hints by IntelliJ IDEA;
Author
makarius
Browse Repository
No Builds
No Audits
3637a0d06fe1 avoid result based on outdated state, e.g. relevant for use_theories with…
Author
makarius
Browse Repository
No Builds
No Audits
43e66527fa93 tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
3e1e2f9198bb tuned signature, following hints by IntelliJ IDEA;
Author
makarius
Browse Repository
No Builds
No Audits
9610ec07e997 more robust treatment of state and events;
Author
makarius
Browse Repository
No Builds
No Audits
085b37d13d41 tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
4556f76d216e proper result state (amending 954640e846d6);
Author
makarius
Browse Repository
No Builds
No Audits
9783e79a37c6 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
7563367690a1 tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
954640e846d6 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
7c0bdb31fdb4 tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
f67e8a557b7d tuned: clarified old_theory (in contrast to 4d5342898b1);
Author
makarius
Browse Repository
No Builds
No Audits
5f6c43eeff90 tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
fab6568b119d more robust: active consumer for check_state/check_progress;
Author
makarius
Browse Repository
No Builds
No Audits
c5c747ce46d2 proper update of non-committed theories (see also 2bf1d0e57695, 2a1583baaaa0);
Author
makarius
Browse Repository
No Builds
No Audits
cf57fd4dd27b tuned;
Author
makarius
Browse Repository
No Builds
No Audits
fdf823f5b56f tuned;
Author
makarius
Browse Repository
No Builds
No Audits
072e6c0a2373 proper Symbol.encode (following fd1efd6dd385), e.g. relevant for 'ML_file' with…
Author
makarius
Browse Repository
No Builds
No Audits

Changes (63)

Path

Size

Admin/

components/

components.sha1

Auth/

CertifiedEmail.thy

Guard/

Guard_NS_Public.thy

Guard_OtwayRees.thy

Guard_Public.thy

Guard_Shared.thy

Guard_Yahalom.thy

KerberosIV_Gets.thy

Kerberos_BAN.thy

Kerberos_BAN_Gets.thy

NS_Public_Bad.thy

OtwayReesBella.thy

OtwayRees_AN.thy

OtwayRees_Bad.thy

Smartcard/

Yahalom_Bad.thy

ZhouGollmann.thy

BNF_Wellorder_Constructions.thy

Computational_Algebra/

Euclidean_Division.thy

Examples/

Gauss_Numbers.thy

Library/

Rounded_Division.thy

Number_Theory/

Tools/

ATP/

atp_problem_generate.ML

Sledgehammer/

sledgehammer_atp_systems.ML

sledgehammer_prover_atp.ML

Wellfounded.thy

Note_on_signed_division_on_words.thy

Pure/

Admin/

isabelle_cronjob.scala

rISABELLE8641f16abc7a

Admin/components/components.sha1

Loading...

CONTRIBUTORS

Loading...

NEWS

Loading...

src/HOL/Auth/CertifiedEmail.thy

Loading...

src/HOL/Auth/Event.thy

Loading...

src/HOL/Auth/Guard/Analz.thy

Loading...

src/HOL/Auth/Guard/Extensions.thy

Loading...

src/HOL/Auth/Guard/Guard.thy

Loading...

src/HOL/Auth/Guard/GuardK.thy

Loading...

src/HOL/Auth/Guard/Guard_NS_Public.thy

Loading...

src/HOL/Auth/Guard/Guard_OtwayRees.thy

Loading...

src/HOL/Auth/Guard/Guard_Public.thy

Loading...

src/HOL/Auth/Guard/Guard_Shared.thy

Loading...

src/HOL/Auth/Guard/Guard_Yahalom.thy

Loading...

src/HOL/Auth/Guard/List_Msg.thy

Loading...

src/HOL/Auth/Guard/P1.thy

Loading...

src/HOL/Auth/Guard/P2.thy

Loading...

src/HOL/Auth/Guard/Proto.thy

Loading...

src/HOL/Auth/KerberosIV.thy

Loading...

src/HOL/Auth/KerberosIV_Gets.thy

Loading...

src/HOL/Auth/KerberosV.thy

Loading...

src/HOL/Auth/Kerberos_BAN.thy

Loading...

src/HOL/Auth/Kerberos_BAN_Gets.thy

Loading...

src/HOL/Auth/Message.thy

Loading...

src/HOL/Auth/NS_Public.thy

Loading...

src/HOL/Auth/NS_Public_Bad.thy

Loading...

src/HOL/Auth/NS_Shared.thy

Loading...

src/HOL/Auth/OtwayRees.thy

Loading...

src/HOL/Auth/OtwayReesBella.thy

Loading...

src/HOL/Auth/OtwayRees_AN.thy

Loading...

src/HOL/Auth/OtwayRees_Bad.thy

Loading...

src/HOL/Auth/Public.thy

Loading...

src/HOL/Auth/Recur.thy

Loading...

src/HOL/Auth/Shared.thy

Loading...

src/HOL/Auth/Smartcard/Smartcard.thy

Loading...

src/HOL/Auth/TLS.thy

Loading...

src/HOL/Auth/WooLam.thy

Loading...

src/HOL/Auth/Yahalom.thy

Loading...

src/HOL/Auth/Yahalom_Bad.thy

Loading...

src/HOL/Auth/ZhouGollmann.thy

Loading...

src/HOL/BNF_Wellorder_Constructions.thy

Loading...

src/HOL/Computational_Algebra/Polynomial.thy

Loading...

src/HOL/Euclidean_Division.thy

Loading...

src/HOL/Examples/Ackermann.thy

Loading...

src/HOL/Examples/Gauss_Numbers.thy

Loading...

src/HOL/Fun.thy

Loading...

src/HOL/Library/FSet.thy

Loading...

src/HOL/Library/Multiset.thy

Loading...

src/HOL/Library/Rounded_Division.thy

Loading...

src/HOL/List.thy

Loading...

src/HOL/Number_Theory/Gauss.thy

Loading...

src/HOL/Relation.thy

Loading...

src/HOL/Set.thy

Loading...

src/HOL/Tools/ATP/atp_problem.ML

Loading...

src/HOL/Tools/ATP/atp_problem_generate.ML

Loading...

src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML

Loading...

src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML

Loading...

src/HOL/Wellfounded.thy

Loading...

src/HOL/ex/Note_on_signed_division_on_words.thy

Loading...

src/Pure/Admin/isabelle_cronjob.scala

Loading...