Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Changes from Mercurial (hg https://bitbucket.org/isa-afp/afp-devel/ default)

Summary

  1. clarified session directories;
  2. clarified session directories;
  3. clarified session directories;
  4. clarified session directories;
  5. clarified session directories;
  6. non-executable source files;
  7. clarified session directories;
Changeset 10588:4dd1561aba40 by wenzelm:
clarified session directories;
The file was addedthys/Berlekamp_Zassenhaus/Pre_BZ/empty
The file was addedthys/CAVA_LTL_Modelchecker/CAVA_Setup/empty
The file was addedthys/CAVA_LTL_Modelchecker/SM_Base/empty
The file was addedthys/Formula_Derivatives/Examples/Presburger_Examples.thy
The file was addedthys/Formula_Derivatives/Examples/WS1S_Alt_Examples.thy
The file was addedthys/Formula_Derivatives/Examples/WS1S_Examples.thy
The file was addedthys/Formula_Derivatives/Examples/WS1S_Nameful_Examples.thy
The file was addedthys/Formula_Derivatives/Examples/WS1S_Presburger_Examples.thy
The file was addedthys/Iptables_Semantics/Examples_Big/empty
The file was addedthys/Ordinary_Differential_Equations/Ex/ARCH_COMP/Examples_ARCH_COMP.thy
The file was addedthys/Ordinary_Differential_Equations/Ex/Lorenz/C0/Lorenz_C0.thy
The file was addedthys/Ordinary_Differential_Equations/Ex/Lorenz/C1/Lorenz_C1.thy
The file was addedthys/Ordinary_Differential_Equations/Ex/ODE_Examples.thy
The file was addedthys/Ordinary_Differential_Equations/Numerics/ODE_Numerics.thy
The file was addedthys/Polynomial_Factorization/Lib/empty
The file was addedthys/Refine_Imperative_HOL/Sepref_Basic/empty
The file was addedthys/Refine_Imperative_HOL/Sepref_IICF/empty
The file was addedthys/Refine_Imperative_HOL/Sepref_Prereq/empty
The file was modified thys/Berlekamp_Zassenhaus/ROOT
The file was modified thys/CAVA_Automata/ROOT
The file was modified thys/CAVA_LTL_Modelchecker/ROOT
The file was modified thys/Collections/ROOT
The file was modified thys/Containers/ROOT
The file was modified thys/Formula_Derivatives/ROOT
The file was modified thys/Iptables_Semantics/ROOT
The file was modified thys/Ordinary_Differential_Equations/ROOT
The file was modified thys/Polynomial_Factorization/ROOT
The file was modified thys/Refine_Imperative_HOL/ROOT
The file was modified thys/Show/ROOT
The file was removedthys/Formula_Derivatives/Presburger_Examples.thy
The file was removedthys/Formula_Derivatives/WS1S_Alt_Examples.thy
The file was removedthys/Formula_Derivatives/WS1S_Examples.thy
The file was removedthys/Formula_Derivatives/WS1S_Nameful_Examples.thy
The file was removedthys/Formula_Derivatives/WS1S_Presburger_Examples.thy
The file was removedthys/Ordinary_Differential_Equations/Ex/Examples_ARCH_COMP.thy
The file was removedthys/Ordinary_Differential_Equations/Ex/Lorenz/Lorenz_C0.thy
The file was removedthys/Ordinary_Differential_Equations/Ex/Lorenz/Lorenz_C1.thy
The file was removedthys/Ordinary_Differential_Equations/ODE_Examples.thy
The file was removedthys/Ordinary_Differential_Equations/ODE_Numerics.thy
Changeset 10587:d97b1078fc97 by wenzelm:
clarified session directories;
The file was modified thys/CakeML/ROOT
Changeset 10586:98b3857f87e4 by wenzelm:
clarified session directories;
The file was addedthys/Linear_Recurrences/Solver/Linear_Recurrences_Pretty.thy
The file was addedthys/Linear_Recurrences/Solver/Linear_Recurrences_Solver.thy
The file was addedthys/Linear_Recurrences/Solver/Linear_Recurrences_Test.thy
The file was addedthys/Linear_Recurrences/Solver/Show_RatFPS.thy
The file was modified thys/Linear_Recurrences/ROOT
The file was removedthys/Linear_Recurrences/Linear_Recurrences_Pretty.thy
The file was removedthys/Linear_Recurrences/Linear_Recurrences_Solver.thy
The file was removedthys/Linear_Recurrences/Linear_Recurrences_Test.thy
The file was removedthys/Linear_Recurrences/Show_RatFPS.thy
Changeset 10585:6f26aeb7cac5 by wenzelm:
clarified session directories;
The file was addedthys/Flyspeck-Tame/Computation/ArchComp.thy
The file was addedthys/Flyspeck-Tame/Computation/Completeness.thy
The file was modified thys/Flyspeck-Tame/ROOT
The file was removedthys/Flyspeck-Tame/ArchComp.thy
The file was removedthys/Flyspeck-Tame/Completeness.thy
Changeset 10584:cc90f69da461 by wenzelm:
clarified session directories;
The file was modified thys/UTP/ROOT
Changeset 10583:1cf4d6f4de8e by wenzelm:
non-executable source files;
The file was modified thys/UTP/ROOT
The file was modified thys/UTP/toolkit/Countable_Set_Extra.thy
The file was modified thys/UTP/toolkit/Finite_Fun.thy
The file was modified thys/UTP/toolkit/Partial_Fun.thy
The file was modified thys/UTP/toolkit/Positive.thy
The file was modified thys/UTP/toolkit/ROOT
The file was modified thys/UTP/toolkit/Sequence.thy
The file was modified thys/UTP/toolkit/Total_Recall.ML
The file was modified thys/UTP/toolkit/Total_Recall.thy
The file was modified thys/UTP/toolkit/utp_toolkit.thy
The file was modified thys/UTP/utp/examples/gcd.thy
The file was modified thys/UTP/utp/utp.thy
The file was modified thys/UTP/utp/utp_dynlog.thy
The file was modified thys/UTP/utp/utp_easy_parser.thy
The file was modified thys/UTP/utp/utp_expr_funcs.thy
The file was modified thys/UTP/utp/utp_expr_insts.thy
The file was modified thys/UTP/utp/utp_full.thy
The file was modified thys/UTP/utp/utp_healthy.thy
The file was modified thys/UTP/utp/utp_rel.thy
The file was modified thys/UTP/utp/utp_sequent.thy
The file was modified thys/UTP/utp/utp_sym_eval.thy
The file was modified thys/UTP/utp/utp_theory.thy
Changeset 10582:838a646468c7 by wenzelm:
clarified session directories;
The file was addedthys/Probabilistic_System_Zoo/BNFs/Bool_Bounded_Set.thy
The file was addedthys/Probabilistic_System_Zoo/BNFs/document/root.tex
The file was addedthys/Probabilistic_System_Zoo/Non_BNFs/document/root.tex
The file was addedthys/Probabilistic_System_Zoo/document/root.tex
The file was modified thys/Probabilistic_System_Zoo/ROOT
The file was removedthys/Probabilistic_System_Zoo/Bool_Bounded_Set.thy
The file was removedthys/Probabilistic_System_Zoo/document/BNFs/root.tex
The file was removedthys/Probabilistic_System_Zoo/document/Hierarchy/root.tex
The file was removedthys/Probabilistic_System_Zoo/document/Non_BNFs/root.tex

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

Summary

  1. theory_name based on session_directories: no need for expensive all_known;
  2. clarified session_directories: relative to session_path, with overlapping information;
  3. clarified signature: retain global session information, unaffected by later restriction;
  4. disable fragile options for now;
  5. avoid overlapping session directories;
  6. support for explicit session directories;
Changeset 70673:b0172698d0d3 by wenzelm:
theory_name based on session_directories: no need for expensive all_known;
The file was modified src/Pure/PIDE/resources.scala
The file was modified src/Pure/Thy/sessions.scala
Changeset 70672:e4bba654d085 by wenzelm:
clarified session_directories: relative to session_path, with overlapping information;
The file was modified src/Pure/Thy/sessions.scala
Changeset 70671:cb1776c8e216 by wenzelm:
clarified signature: retain global session information, unaffected by later restriction;
The file was modified src/Pure/Thy/sessions.scala
The file was modified src/Pure/Tools/build.scala
Changeset 70670:a1dfd603260e by wenzelm:
disable fragile options for now;
The file was modified src/Pure/Tools/dump.scala
Changeset 70669:abdf3732f6f1 by wenzelm:
avoid overlapping session directories;
The file was modified src/HOL/ROOT
Changeset 70668:9cac4dec0da9 by wenzelm:
support for explicit session directories;
The file was modified src/Pure/Isar/parse.scala
The file was modified src/Pure/Sessions.thy
The file was modified src/Pure/Thy/sessions.ML
The file was modified src/Pure/Thy/sessions.scala