Skip to content
Success

Changes

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

Summary

  1. more operations on types and terms; abstract syntax operations for Pure and HOL;
  2. clarified jEdit java sources;
  3. clarified build.gradle: "compile" stopped working in gradle 6.x / 7.x for unknown reasons;
  4. removed junk;
  5. moved theory Bit_Operations into Main corpus
Changeset 74105:d3d6e01a6b00 by wenzelm:
more operations on types and terms;<br>abstract syntax operations for Pure and HOL;
The file was modified src/Tools/Haskell/Haskell.thy
The file was modified src/Tools/ROOT
Changeset 74104:fa92c5f8af86 by wenzelm:
clarified jEdit java sources;
The file was modified Admin/components/components.sha1
The file was modified Admin/components/main
The file was modified src/Pure/Admin/build_jedit.scala
The file was modified src/Pure/Tools/scala_project.scala
Changeset 74103:3b56d00ac333 by wenzelm:
clarified build.gradle: &quot;compile&quot; stopped working in gradle 6.x / 7.x for unknown reasons;
The file was modified src/Pure/Tools/scala_project.scala
Changeset 74102:0572c733d12d by wenzelm:
removed junk;
The file was modified src/HOL/Main.thy
Changeset 74101:d804e93ae9ff by haftmann:
moved theory Bit_Operations into Main corpus
The file was addedsrc/HOL/Bit_Operations.thy
The file was addedsrc/HOL/Boolean_Algebra.thy
The file was modified NEWS
The file was modified src/HOL/Code_Numeral.thy
The file was modified src/HOL/Decision_Procs/Cooper.thy
The file was modified src/HOL/Decision_Procs/Ferrack.thy
The file was modified src/HOL/Decision_Procs/MIR.thy
The file was modified src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
The file was modified src/HOL/Divides.thy
The file was modified src/HOL/Fun.thy
The file was modified src/HOL/GCD.thy
The file was modified src/HOL/Groups_List.thy
The file was modified src/HOL/HOLCF/IOA/Pred.thy
The file was modified src/HOL/IMP/OO.thy
The file was modified src/HOL/Library/Library.thy
The file was modified src/HOL/Library/Linear_Temporal_Logic_on_Streams.thy
The file was modified src/HOL/Library/Word.thy
The file was modified src/HOL/Library/Z2.thy
The file was modified src/HOL/List.thy
The file was modified src/HOL/Main.thy
The file was modified src/HOL/Nominal/Examples/Class1.thy
The file was modified src/HOL/Numeral_Simprocs.thy
The file was modified src/HOL/Parity.thy
The file was modified src/HOL/Random.thy
The file was modified src/HOL/Set.thy
The file was modified src/HOL/Set_Interval.thy
The file was modified src/HOL/String.thy
The file was modified src/HOL/ex/Meson_Test.thy
The file was modified src/HOL/ex/Reflection_Examples.thy
The file was modified src/HOL/ex/Tree23.thy
The file was removedsrc/HOL/Library/Bit_Operations.thy
The file was removedsrc/HOL/Library/Boolean_Algebra.thy

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

Summary

  1. restored executable conversions
  2. dropped junk
  3. moved theory Bit_Operations into Main corpus
Changeset 11949:da7fd1ac6b66 by haftmann:
restored executable conversions
The file was modified thys/Native_Word/Native_Word_Test.thy
The file was modified thys/Native_Word/Uint16.thy
The file was modified thys/Native_Word/Uint32.thy
The file was modified thys/Native_Word/Uint64.thy
The file was modified thys/Native_Word/Uint8.thy
Changeset 11948:7f4f3900fd58 by haftmann:
dropped junk
The file was removedthys/Word_Lib/Word_Setup_32.thy
The file was removedthys/Word_Lib/Word_Setup_64.thy
Changeset 11947:c341fdde0cba by haftmann:
moved theory Bit_Operations into Main corpus
The file was modified thys/Amortized_Complexity/Splay_Tree_Analysis.thy
The file was modified thys/BDD/General.thy
The file was modified thys/Formula_Derivatives/Presburger_Formula.thy
The file was modified thys/Isabelle_Meta_Model/meta_isabelle/Meta_Isabelle.thy
The file was modified thys/Knot_Theory/Preliminaries.thy
The file was modified thys/Monad_Normalisation/Monad_Normalisation_Test.thy
The file was modified thys/MonoBoolTranAlgebra/Statements.thy
The file was modified thys/Order_Lattice_Props/Order_Duality.thy
The file was modified thys/Order_Lattice_Props/Order_Lattice_Props.thy
The file was modified thys/Order_Lattice_Props/Order_Lattice_Props_Loc.thy
The file was modified thys/Order_Lattice_Props/Order_Lattice_Props_Wenzel.thy
The file was modified thys/Order_Lattice_Props/Representations.thy
The file was modified thys/Relation_Algebra/More_Boolean_Algebra.thy
The file was modified thys/Relation_Algebra/Relation_Algebra_Models.thy
The file was modified thys/Residuated_Lattices/Residuated_Boolean_Algebras.thy
The file was modified thys/Residuated_Lattices/Residuated_Relation_Algebra.thy
The file was modified thys/Robbins-Conjecture/Robbins_Conjecture.thy
The file was modified thys/Statecharts/Expr.thy
The file was modified thys/Stone_Algebras/Lattice_Basics.thy
The file was modified thys/Stone_Algebras/P_Algebras.thy
The file was modified thys/Stone_Relation_Algebras/Linear_Order_Matrices.thy
The file was modified thys/Stone_Relation_Algebras/Matrix_Relation_Algebras.thy
The file was modified thys/Subset_Boolean_Algebras/Subset_Boolean_Algebras.thy
The file was modified thys/UTP/utp/utp_pred_laws.thy
The file was modified thys/Word_Lib/Guide.thy
The file was modified thys/Word_Lib/More_Arithmetic.thy
The file was modified thys/Word_Lib/More_Word.thy
The file was modified thys/Word_Lib/Word_Lemmas.thy