Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Changes from Mercurial (hg http://isabelle.in.tum.de/repos/isabelle/ default)

Summary

  1. tuned signature;
  2. check imports more strictly, e.g. reject ".../Pure" or ".../HOL-Library.Multiset";
  3. tuned signature;
  4. tuned --- more robust syntax;
  5. tuned signature;
  6. back to more traditional import_name (reverting cceb10dcc9f9), e.g. relevant for "isabelle jedit -l CTT src/CTT/ex/Elimination.thy" to produce proper error "Cannot update finished theory CTT.Elimination";
  7. unused (see 347ed6219dab);
  8. tuned signature;
Changeset 76051:854e9223767f by wenzelm:
tuned signature;
The file was modified src/HOL/Library/conditional_parametricity.ML
The file was modified src/Pure/goal.ML
The file was modified src/Pure/tactical.ML
Changeset 76050:f1dc3d9d5164 by wenzelm:
check imports more strictly, e.g. reject ".../Pure" or ".../HOL-Library.Multiset";
The file was modified src/Pure/PIDE/resources.ML
The file was modified src/Pure/PIDE/resources.scala
Changeset 76049:d6c6e787cd86 by wenzelm:
tuned signature;
The file was modified src/Pure/PIDE/resources.ML
The file was modified src/Pure/PIDE/resources.scala
Changeset 76048:92aa9ac31c7c by wenzelm:
tuned --- more robust syntax;
The file was modified src/Pure/Thy/sessions.scala
Changeset 76047:f244926013e5 by wenzelm:
tuned signature;
The file was modified src/Pure/Isar/proof.ML
The file was modified src/Pure/goal.ML
The file was modified src/Pure/term.ML
Changeset 76046:507c65cc4332 by wenzelm:
back to more traditional import_name (reverting cceb10dcc9f9), e.g. relevant for "isabelle jedit -l CTT src/CTT/ex/Elimination.thy" to produce proper error "Cannot update finished theory CTT.Elimination";
The file was modified src/Pure/PIDE/resources.ML
The file was modified src/Pure/PIDE/resources.scala
Changeset 76045:4aeb5f019e53 by wenzelm:
unused (see 347ed6219dab);
The file was modified src/Pure/PIDE/session.scala
Changeset 76044:c90799513ed0 by wenzelm:
tuned signature;
The file was modified src/Tools/jEdit/src/jedit_editor.scala

Changes from Mercurial (hg https://foss.heptapod.net/isa-afp/afp-devel/ default)

Summary

  1. tuned signature;
  2. merged
  3. Substantial additions by Franz Regensburger to the Universal_Turing_Machine entry
  4. tuned timeouts, based on test runs with threads=1;
Changeset 12967:6c87f24bb773 by wenzelm:
tuned signature;
The file was modified thys/Refine_Imperative_HOL/Sepref_Basic.thy
Changeset 12966:14eb275d680e by Christian Urban _christian.urban@kcl.ac.uk_:
merged
Changeset 12965:f294e5dddd66 by Christian Urban _christian.urban@kcl.ac.uk_:
Substantial additions by Franz Regensburger to the Universal_Turing_Machine entry
The file was addedthys/Universal_Turing_Machine/Abacus_alt_Compile.thy
The file was addedthys/Universal_Turing_Machine/BlanksDoNotMatter.thy
The file was addedthys/Universal_Turing_Machine/CHANGELOG
The file was addedthys/Universal_Turing_Machine/ComposableTMs.thy
The file was addedthys/Universal_Turing_Machine/ComposableTMs_aux.thy
The file was addedthys/Universal_Turing_Machine/ComposedTMs.thy
The file was addedthys/Universal_Turing_Machine/CopyTM.thy
The file was addedthys/Universal_Turing_Machine/DitherTM.thy
The file was addedthys/Universal_Turing_Machine/GeneratedCode.thy
The file was addedthys/Universal_Turing_Machine/HaltingProblems_K_H.thy
The file was addedthys/Universal_Turing_Machine/HaltingProblems_K_aux.thy
The file was addedthys/Universal_Turing_Machine/Numerals.thy
The file was addedthys/Universal_Turing_Machine/Numerals_Ex.thy
The file was addedthys/Universal_Turing_Machine/OneStrokeTM.thy
The file was addedthys/Universal_Turing_Machine/Rec_Ex.thy
The file was addedthys/Universal_Turing_Machine/Recs_alt_Def.thy
The file was addedthys/Universal_Turing_Machine/Recs_alt_Ex.thy
The file was addedthys/Universal_Turing_Machine/SemiIdTM.thy
The file was addedthys/Universal_Turing_Machine/SimpleGoedelEncoding.thy
The file was addedthys/Universal_Turing_Machine/StrongCopyTM.thy
The file was addedthys/Universal_Turing_Machine/TM_Playground.thy
The file was addedthys/Universal_Turing_Machine/TuringComputable.thy
The file was addedthys/Universal_Turing_Machine/TuringComputable_aux.thy
The file was addedthys/Universal_Turing_Machine/TuringDecidable.thy
The file was addedthys/Universal_Turing_Machine/TuringReducible.thy
The file was addedthys/Universal_Turing_Machine/TuringUnComputable_H2.thy
The file was addedthys/Universal_Turing_Machine/TuringUnComputable_H2_original.thy
The file was addedthys/Universal_Turing_Machine/Turing_HaltingConditions.thy
The file was addedthys/Universal_Turing_Machine/Turing_aux.thy
The file was addedthys/Universal_Turing_Machine/WeakCopyTM.thy
The file was modified thys/Universal_Turing_Machine/Abacus.thy
The file was modified thys/Universal_Turing_Machine/Abacus_Hoare.thy
The file was modified thys/Universal_Turing_Machine/Abacus_Mopup.thy
The file was modified thys/Universal_Turing_Machine/ROOT
The file was modified thys/Universal_Turing_Machine/Rec_Def.thy
The file was modified thys/Universal_Turing_Machine/Recursive.thy
The file was modified thys/Universal_Turing_Machine/Turing.thy
The file was modified thys/Universal_Turing_Machine/Turing_Hoare.thy
The file was modified thys/Universal_Turing_Machine/UF.thy
The file was modified thys/Universal_Turing_Machine/UTM.thy
The file was modified thys/Universal_Turing_Machine/document/root.bib
The file was modified thys/Universal_Turing_Machine/document/root.tex
Changeset 12964:5a1267ab6b71 by wenzelm:
tuned timeouts, based on test runs with threads=1;
The file was modified thys/BTree/ROOT
The file was modified thys/CZH_Elementary_Categories/ROOT
The file was modified thys/Category3/ROOT
The file was modified thys/Complex_Bounded_Operators/ROOT
The file was modified thys/FSM_Tests/ROOT
The file was modified thys/Solidity/ROOT