Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. tuned --- following hints by IntelliJ;
  2. tuned signature;
  3. tuned;
  4. tuned;
  5. tuned signature;
  6. tuned;
  7. tuned signature (see 2d6a489adb01);
  8. added support for TFX's and THF's $ite to Sledgehammer
  9. tuned Mirabelle documentation
  10. shortened long lines
  11. fixed typos
  12. updated Mirabelle documentation
  13. changed Mirabelle's filter to use short theory names
  14. more lemmas
Changeset 73866:66bff50bc5f1 by wenzelm:
tuned --- following hints by IntelliJ;
The file was modified src/Pure/Thy/export_theory.scala
Changeset 73865:4e94ceabaaad by wenzelm:
tuned signature;
The file was modified src/Pure/library.ML
Changeset 73864:ac5a72740f3a by wenzelm:
tuned;
The file was modified src/Pure/General/position.ML
Changeset 73863:9594d8e33c57 by wenzelm:
tuned;
The file was modified src/Pure/term_ord.ML
Changeset 73862:38fe15a42ff2 by wenzelm:
tuned signature;
The file was modified src/Pure/library.ML
Changeset 73861:aa0b1fbe6be3 by wenzelm:
tuned;
The file was modified src/Pure/library.ML
Changeset 73860:dfac078e5444 by wenzelm:
tuned signature (see 2d6a489adb01);
The file was modified src/Pure/library.ML
The file was modified src/Pure/more_thm.ML
The file was modified src/Pure/thm.ML
Changeset 73859:bc263f1f68cd by desharna:
added support for TFX's and THF's $ite to Sledgehammer
The file was modified src/Doc/Sledgehammer/document/root.tex
The file was modified src/HOL/Tools/ATP/atp_problem.ML
The file was modified src/HOL/Tools/ATP/atp_problem_generate.ML
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
Changeset 73858:4538d6ffafbd by desharna:
tuned Mirabelle documentation
The file was modified src/Doc/Sledgehammer/document/root.tex
Changeset 73857:a88427e55371 by desharna:
shortened long lines
The file was modified src/Doc/Sledgehammer/document/root.tex
Changeset 73856:07675be65227 by desharna:
fixed typos
The file was modified src/Doc/Sledgehammer/document/root.tex
Changeset 73855:c55980cf7374 by desharna:
updated Mirabelle documentation
The file was modified src/Doc/Sledgehammer/document/root.tex
Changeset 73854:eab5cd9c7862 by desharna:
changed Mirabelle's filter to use short theory names
The file was modified src/HOL/Tools/Mirabelle/mirabelle.ML
Changeset 73853:52b829b18066 by haftmann:
more lemmas
The file was modified src/HOL/Euclidean_Division.thy
The file was modified src/HOL/Library/Word.thy
The file was modified src/HOL/Parity.thy

Summary

  1. Relational_Disjoint_Set_Forests: updated metadata to reflect added theory
  2. Relational_Disjoint_Set_Forests: add theory More_Disjoint_Set_Forests
  3. lemma grooming
  4. no duplicates of shift operations
  5. merge Jinja/Isar work
  6. updated change history for Interpreter_Optimization
  7. merged
  8. updated, replacing axiomatizations by proper locales
  9. added basic blocks
  10. Updating Jinja from apply-style to Isar-style
  11. Updating Jinja from apply-style to Isar-style
  12. Updating Jinja from apply-style to Isar-style
  13. Updating Jinja from apply-style to Isar-style
  14. Updating Jinja from apply-style to Isar-style
  15. Updating Jinja from apply-style to Isar-style
  16. Updating Jinja from apply-style to Isar-style
  17. Updating Jinja from apply-style to Isar-style
  18. Updating Jinja from apply-style to Isar-style
  19. Updating Jinja from apply-style to Isar-style
  20. Updating Jinja from apply-style to Isar-style
  21. Updating Jinja from apply-style to Isar-style
  22. Updating Jinja from apply-style to Isar-style
  23. Merge from default, esp JinjaDCI
  24. Updating Jinja from apply-style to Isar-style
  25. Updating Jinja from apply-style to Isar-style
Changeset 11883:7b56a9ce5619 by walter guttmann _walter.guttmann@canterbury.ac.nz_:
Relational_Disjoint_Set_Forests: updated metadata to reflect added theory
The file was modified metadata/metadata
Changeset 11882:98c7aa03457d by walter guttmann _walter.guttmann@canterbury.ac.nz_:
Relational_Disjoint_Set_Forests: add theory More_Disjoint_Set_Forests
The file was addedthys/Relational_Disjoint_Set_Forests/More_Disjoint_Set_Forests.thy
The file was modified thys/Relational_Disjoint_Set_Forests/Disjoint_Set_Forests.thy
The file was modified thys/Relational_Disjoint_Set_Forests/ROOT
The file was modified thys/Relational_Disjoint_Set_Forests/document/root.tex
The file was modified thys/Stone_Algebras/P_Algebras.thy
The file was modified thys/Stone_Kleene_Relation_Algebras/Kleene_Relation_Algebras.thy
The file was modified thys/Stone_Relation_Algebras/Relation_Algebras.thy
Changeset 11881:06eb6c7d6c76 by haftmann:
lemma grooming
The file was modified thys/IEEE_Floating_Point/Conversion_IEEE_Float.thy
The file was modified thys/IEEE_Floating_Point/IEEE_Properties.thy
The file was modified thys/Iptables_Semantics/Common/Word_Upto.thy
The file was modified thys/Word_Lib/Aligned.thy
The file was modified thys/Word_Lib/Bits_Int.thy
The file was modified thys/Word_Lib/Enumeration_Word.thy
The file was modified thys/Word_Lib/More_Word.thy
The file was modified thys/Word_Lib/Typedef_Morphisms.thy
The file was modified thys/Word_Lib/Word_Lemmas.thy
Changeset 11880:c2595f7c289f by haftmann:
no duplicates of shift operations
The file was addedthys/Word_Lib/Bit_Shifts_Infix_Syntax.thy
The file was modified thys/Algebraic_Numbers/Real_Roots.thy
The file was modified thys/Berlekamp_Zassenhaus/Finite_Field_Record_Based.thy
The file was modified thys/CakeML/generated/Lem_word.thy
The file was modified thys/IP_Addresses/IPv4.thy
The file was modified thys/IP_Addresses/IPv6.thy
The file was modified thys/IP_Addresses/NumberWang_IPv6.thy
The file was modified thys/IP_Addresses/Prefix_Match.thy
The file was modified thys/JinjaThreads/Common/BinOp.thy
The file was modified thys/Mersenne_Primes/Lucas_Lehmer_Code.thy
The file was modified thys/Native_Word/Bits_Integer.thy
The file was modified thys/Native_Word/Code_Symbolic_Bits_Int.thy
The file was modified thys/Native_Word/Code_Target_Word_Base.thy
The file was modified thys/Native_Word/Native_Word_Test.thy
The file was modified thys/Native_Word/Native_Word_Test_Scala.thy
The file was modified thys/Native_Word/Uint.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
The file was modified thys/SPARCv8/SparcModel_MMU/RegistersOps.thy
The file was modified thys/SPARCv8/SparcModel_MMU/Sparc_Types.thy
The file was modified thys/Word_Lib/Aligned.thy
The file was modified thys/Word_Lib/Ancient_Numeral.thy
The file was modified thys/Word_Lib/Bits_Int.thy
The file was modified thys/Word_Lib/Bitwise.thy
The file was modified thys/Word_Lib/Generic_set_bit.thy
The file was modified thys/Word_Lib/Guide.thy
The file was modified thys/Word_Lib/Least_significant_bit.thy
The file was modified thys/Word_Lib/More_Arithmetic.thy
The file was modified thys/Word_Lib/More_Divides.thy
The file was modified thys/Word_Lib/More_Word_Operations.thy
The file was modified thys/Word_Lib/Most_significant_bit.thy
The file was modified thys/Word_Lib/Reversed_Bit_Lists.thy
The file was modified thys/Word_Lib/Rsplit.thy
The file was modified thys/Word_Lib/Typedef_Morphisms.thy
The file was modified thys/Word_Lib/Word_32.thy
The file was modified thys/Word_Lib/Word_64.thy
The file was modified thys/Word_Lib/Word_EqI.thy
The file was modified thys/Word_Lib/Word_Lemmas.thy
The file was modified thys/Word_Lib/Word_Lib_Sumo.thy
The file was removedthys/Word_Lib/Traditional_Infix_Syntax.thy
Changeset 11879:2e179108e08f by gerwin klein _kleing@unsw.edu.au_:
merge Jinja/Isar work
Changeset 11878:5e24878a9118 by desharna:
updated change history for Interpreter_Optimization
The file was modified metadata/metadata
Changeset 11877:29da90822fc7 by paulson:
merged
Changeset 11876:a51be9ca4b87 by paulson _lp15@cam.ac.uk_:
updated, replacing axiomatizations by proper locales
The file was modified thys/Projective_Geometry/Desargues_2D.thy
The file was modified thys/Projective_Geometry/Desargues_3D.thy
The file was modified thys/Projective_Geometry/Desargues_Property.thy
The file was modified thys/Projective_Geometry/Higher_Projective_Space_Axioms.thy
The file was modified thys/Projective_Geometry/Higher_Projective_Space_Rank_Axioms.thy
The file was modified thys/Projective_Geometry/Matroid_Rank_Properties.thy
The file was modified thys/Projective_Geometry/Pappus_Desargues.thy
The file was modified thys/Projective_Geometry/Pappus_Property.thy
The file was modified thys/Projective_Geometry/Pascal_Property.thy
The file was modified thys/Projective_Geometry/Projective_Plane_Axioms.thy
The file was modified thys/Projective_Geometry/Projective_Space_Axioms.thy
Changeset 11875:95f457f69761 by desharna:
added basic blocks
The file was addedthys/Interpreter_Optimizations/AList_Extra.thy
The file was addedthys/Interpreter_Optimizations/Map_Extra.thy
The file was addedthys/Interpreter_Optimizations/Option_Extra.thy
The file was addedthys/Interpreter_Optimizations/Ubx_Verification.thy
The file was modified thys/Interpreter_Optimizations/Dynamic.thy
The file was modified thys/Interpreter_Optimizations/Env.thy
The file was modified thys/Interpreter_Optimizations/Env_list.thy
The file was modified thys/Interpreter_Optimizations/Global.thy
The file was modified thys/Interpreter_Optimizations/Inca.thy
The file was modified thys/Interpreter_Optimizations/Inca_to_Ubx_compiler.thy
The file was modified thys/Interpreter_Optimizations/Inca_to_Ubx_simulation.thy
The file was modified thys/Interpreter_Optimizations/List_util.thy
The file was modified thys/Interpreter_Optimizations/Op.thy
The file was modified thys/Interpreter_Optimizations/OpUbx.thy
The file was modified thys/Interpreter_Optimizations/Op_example.thy
The file was modified thys/Interpreter_Optimizations/ROOT
The file was modified thys/Interpreter_Optimizations/Std.thy
The file was modified thys/Interpreter_Optimizations/Std_to_Inca_compiler.thy
The file was modified thys/Interpreter_Optimizations/Std_to_Inca_simulation.thy
The file was modified thys/Interpreter_Optimizations/Ubx.thy
The file was modified thys/Interpreter_Optimizations/Unboxed.thy
The file was modified thys/Interpreter_Optimizations/Unboxed_lemmas.thy
The file was removedthys/Interpreter_Optimizations/Option_applicative.thy
The file was removedthys/Interpreter_Optimizations/Ubx_type_inference.thy
Changeset 11657:3b6c0a05c5cf by susannah mansky _susannahej@gmail.com_:
Updating Jinja from apply-style to Isar-style
The file was modified thys/Jinja/Compiler/TypeComp.thy
The file was modified thys/JinjaDCI/Compiler/TypeComp.thy
Changeset 11642:158c475e011a by susannah mansky _susannahej@gmail.com_:
Updating Jinja from apply-style to Isar-style
The file was modified thys/Jinja/Compiler/Correctness1.thy
The file was modified thys/Jinja/Compiler/Correctness2.thy
The file was modified thys/Jinja/Compiler/J1.thy
The file was modified thys/Jinja/Compiler/J1WellForm.thy
The file was modified thys/Jinja/Compiler/PCompiler.thy
The file was modified thys/JinjaDCI/Compiler/Correctness1.thy
The file was modified thys/JinjaDCI/Compiler/Correctness2.thy
The file was modified thys/JinjaDCI/Compiler/J1.thy
The file was modified thys/JinjaDCI/Compiler/J1WellForm.thy
The file was modified thys/JinjaDCI/Compiler/PCompiler.thy
Changeset 11626:3e4722b88fc2 by susannah mansky _susannahej@gmail.com_:
Updating Jinja from apply-style to Isar-style
The file was modified thys/Jinja/J/Equivalence.thy
The file was modified thys/JinjaDCI/J/Equivalence.thy
Changeset 11625:a1007d72329d by susannah mansky _susannahej@gmail.com_:
Updating Jinja from apply-style to Isar-style
The file was modified thys/Jinja/J/Equivalence.thy
The file was modified thys/JinjaDCI/J/Equivalence.thy
Changeset 11624:918ccd4df9fe by susannah mansky _susannahej@gmail.com_:
Updating Jinja from apply-style to Isar-style
The file was modified thys/Jinja/J/Equivalence.thy
The file was modified thys/JinjaDCI/J/Equivalence.thy
Changeset 11623:3c89665fe122 by susannah mansky _susannahej@gmail.com_:
Updating Jinja from apply-style to Isar-style
The file was modified thys/Jinja/J/Equivalence.thy
The file was modified thys/JinjaDCI/J/Equivalence.thy
Changeset 11622:b713f1aa07d6 by susannah mansky _susannahej@gmail.com_:
Updating Jinja from apply-style to Isar-style
The file was modified thys/Jinja/J/Equivalence.thy
The file was modified thys/JinjaDCI/J/Equivalence.thy
Changeset 11618:c92e3097a0b8 by susannah mansky _susannahej@gmail.com_:
Updating Jinja from apply-style to Isar-style
The file was modified thys/Jinja/J/TypeSafe.thy
The file was modified thys/JinjaDCI/J/EConform.thy
The file was modified thys/JinjaDCI/J/Equivalence.thy
The file was modified thys/JinjaDCI/J/TypeSafe.thy
Changeset 11617:034574b588e5 by susannah mansky _susannahej@gmail.com_:
Updating Jinja from apply-style to Isar-style
The file was modified thys/Jinja/J/DefAss.thy
The file was modified thys/Jinja/J/JWellForm.thy
The file was modified thys/Jinja/J/Progress.thy
The file was modified thys/JinjaDCI/J/DefAss.thy
The file was modified thys/JinjaDCI/J/EConform.thy
The file was modified thys/JinjaDCI/J/JWellForm.thy
The file was modified thys/JinjaDCI/J/Progress.thy
Changeset 11616:b97c4662e51f by susannah mansky _susannahej@gmail.com_:
Updating Jinja from apply-style to Isar-style
The file was modified thys/Jinja/J/BigStep.thy
The file was modified thys/Jinja/J/Expr.thy
The file was modified thys/Jinja/J/WellType.thy
The file was modified thys/Jinja/J/WellTypeRT.thy
The file was modified thys/JinjaDCI/J/Expr.thy
The file was modified thys/JinjaDCI/J/SmallStep.thy
The file was modified thys/JinjaDCI/J/WWellForm.thy
The file was modified thys/JinjaDCI/J/WellType.thy
The file was modified thys/JinjaDCI/J/WellTypeRT.thy
Changeset 11615:8bb4e3809bd9 by susannah mansky _susannahej@gmail.com_:
Updating Jinja from apply-style to Isar-style
The file was modified thys/Jinja/BV/BVNoTypeError.thy
The file was modified thys/JinjaDCI/BV/BVNoTypeError.thy
Changeset 11603:ed4bb4b543ce by susannah mansky _susannahej@gmail.com_:
Updating Jinja from apply-style to Isar-style
The file was modified thys/Jinja/BV/BVSpecTypeSafe.thy
The file was modified thys/JinjaDCI/BV/BVSpecTypeSafe.thy
Changeset 11602:d75706d3548c by susannah mansky _susannahej@gmail.com_:
Updating Jinja from apply-style to Isar-style
The file was modified thys/JinjaDCI/BV/BVConform.thy
The file was modified thys/JinjaDCI/BV/BVExec.thy
The file was modified thys/JinjaDCI/BV/BVSpec.thy
The file was modified thys/JinjaDCI/BV/Effect.thy
The file was modified thys/JinjaDCI/BV/LBVJVM.thy
The file was modified thys/JinjaDCI/BV/TF_JVM.thy
Changeset 11601:6d1a140d53a0 by susannah mansky _susannahej@gmail.com_:
Merge from default, esp JinjaDCI
Changeset 11600:5090fd532062 by susannah mansky _susannahej@gmail.com_:
Updating Jinja from apply-style to Isar-style
The file was modified thys/Jinja/BV/BVConform.thy
Changeset 11584:944776fde110 by susannah mansky _susannahej@gmail.com_:
Updating Jinja from apply-style to Isar-style
The file was modified thys/Jinja/BV/BVExec.thy
The file was modified thys/Jinja/BV/BVSpec.thy
The file was modified thys/Jinja/BV/Effect.thy
The file was modified thys/Jinja/BV/LBVJVM.thy
The file was modified thys/Jinja/BV/TF_JVM.thy
The file was modified thys/Jinja/Common/Auxiliary.thy
The file was modified thys/Jinja/Common/Conform.thy
The file was modified thys/Jinja/Common/Decl.thy
The file was modified thys/Jinja/Common/Objects.thy
The file was modified thys/Jinja/Common/TypeRel.thy
The file was modified thys/Jinja/Common/WellForm.thy
The file was modified thys/Jinja/JVM/JVMDefensive.thy
The file was modified thys/Jinja/JVM/JVMExec.thy