Skip to content
[Jenkins]Jenkins
log in
Failed

Changes

Summary

  1. more Isabelle/Haskell;
  2. made sure lambda-lifting works well with native let binders in Sledgehammer
  3. handle Zipperposition's ResourceOut gracefully
  4. disabled 'ite' in Zipperposition until we upgrade to a version of Zip that supports it and we generate the proper syntax
  5. proper test for type constructor;
  6. more Isabelle/Haskell operations;
  7. more Isabelle/Haskell operations;
  8. merged
  9. tuned;
  10. more scalable data structure (but: rarely used with > 5 arguments);
  11. Backed out changeset d4af818e0880
  12. merged
  13. more Isabelle/Haskell operations;
  14. more Isabelle/Haskell operations;
  15. tuned;
  16. more Isabelle/Haskell operations;
  17. reflect moved theories
  18. unhide canonical function def examples
  19. merged
  20. merged
  21. Backed out changeset fe8d0f4da0e6
  22. more Isabelle/Haskell operations;
  23. more Isabelle/Haskell operations;
  24. more Isabelle/Haskell operations;
  25. more Isabelle/Haskell operations;
  26. clarified signature;
  27. clarified signature;
  28. minor performance tuning;
  29. tuned;
  30. tuned;
  31. tuned signature;
  32. tuned comments;
  33. treat Symbol.eof as in ML (but: presently unused);
  34. tuned;
  35. minor performance tuning;
  36. clarified signature;
  37. proper Isabelle symbol positions;
  38. more Haskell operations;
  39. clarified signature;
  40. tuned;
  41. tuned;
  42. tuned signature: prefer existing Haskell operations;
  43. more Haskell operations;
  44. tuned signature;
  45. tuned comments;
  46. tuned;
  47. consolidation of rules for bit operations
Changeset 74209:24a2a6ced0ab by wenzelm:
more Isabelle/Haskell;
The file was modified src/Tools/Haskell/Haskell.thy
Changeset 74208:1a8d8dd77513 by blanchet:
made sure lambda-lifting works well with native let binders in Sledgehammer
The file was modified src/HOL/Tools/ATP/atp_problem_generate.ML
Changeset 74207:adf767b94f77 by blanchet:
handle Zipperposition's ResourceOut gracefully
The file was modified src/HOL/Tools/ATP/atp_proof.ML
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
Changeset 74206:9c6159cbf9ee by blanchet:
disabled 'ite' in Zipperposition until we upgrade to a version of Zip that supports it and we generate the proper syntax
The file was modified src/HOL/Tools/Sledgehammer/sledgehammer_atp_systems.ML
Changeset 74205:5f0f0553762f by wenzelm:
proper test for type constructor;
The file was modified src/Tools/Haskell/Haskell.thy
Changeset 74204:c832f35ea571 by wenzelm:
more Isabelle/Haskell operations;
The file was modified src/Tools/Haskell/Haskell.thy
Changeset 74203:92f08f3d77bd by wenzelm:
more Isabelle/Haskell operations;
The file was modified src/Tools/Haskell/Haskell.thy
Changeset 74202:10455384a3e5 by wenzelm:
merged
Changeset 74201:c36b663ef037 by wenzelm:
tuned;
The file was modified src/Pure/variable.ML
Changeset 74200:17090e27aae9 by wenzelm:
more scalable data structure (but: rarely used with > 5 arguments);
The file was modified src/Doc/Implementation/Logic.thy
The file was modified src/HOL/Eisbach/match_method.ML
The file was modified src/HOL/Library/cconv.ML
The file was modified src/HOL/Library/code_lazy.ML
The file was modified src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
The file was modified src/HOL/Tools/BNF/bnf_gfp_rec_sugar_tactics.ML
The file was modified src/HOL/Tools/Ctr_Sugar/ctr_sugar_code.ML
The file was modified src/HOL/Tools/Function/induction_schema.ML
The file was modified src/HOL/Tools/SMT/smt_replay_methods.ML
The file was modified src/HOL/Tools/Transfer/transfer.ML
The file was modified src/Pure/Isar/local_defs.ML
The file was modified src/Pure/drule.ML
The file was modified src/Pure/goal.ML
The file was modified src/Pure/more_thm.ML
The file was modified src/Pure/proofterm.ML
The file was modified src/Pure/term_subst.ML
The file was modified src/Pure/thm.ML
The file was modified src/Pure/variable.ML
Changeset 74199:bf9871795aeb by kevin kappelmann _kevin.kappelmann@tum.de_:
Backed out changeset d4af818e0880
The file was modified src/Tools/ROOT
The file was removedsrc/Tools/Spec_Check/Examples.thy
The file was removedsrc/Tools/Spec_Check/README
The file was removedsrc/Tools/Spec_Check/Spec_Check.thy
The file was removedsrc/Tools/Spec_Check/base_generator.ML
The file was removedsrc/Tools/Spec_Check/gen_construction.ML
The file was removedsrc/Tools/Spec_Check/generator.ML
The file was removedsrc/Tools/Spec_Check/output_style.ML
The file was removedsrc/Tools/Spec_Check/property.ML
The file was removedsrc/Tools/Spec_Check/random.ML
The file was removedsrc/Tools/Spec_Check/spec_check.ML
Changeset 74198:f54b061c2c22 by wenzelm:
merged
Changeset 74197:1f78a40e4399 by wenzelm:
more Isabelle/Haskell operations;
The file was modified src/Tools/Haskell/Haskell.thy
Changeset 74196:6dc7ff326906 by wenzelm:
more Isabelle/Haskell operations;
The file was modified src/Tools/Haskell/Haskell.thy
Changeset 74195:30e2e44baa57 by wenzelm:
tuned;
The file was modified src/Tools/Haskell/Haskell.thy
Changeset 74194:ffe24c7da1c6 by wenzelm:
more Isabelle/Haskell operations;
The file was modified src/Tools/Haskell/Haskell.thy
Changeset 74193:2b00c267196e by nipkow:
reflect moved theories
The file was modified src/HOL/ROOT
Changeset 74192:852df4f1dbfa by nipkow:
unhide canonical function def examples
The file was addedsrc/HOL/Examples/Functions.thy
The file was removedsrc/HOL/ex/Functions.thy
Changeset 74191:ec947c18e060 by nipkow:
merged
Changeset 74190:9a1796acd0a4 by nipkow:
merged
Changeset 74189:d4af818e0880 by nipkow:
Backed out changeset fe8d0f4da0e6
The file was addedsrc/Tools/Spec_Check/Examples.thy
The file was addedsrc/Tools/Spec_Check/README
The file was addedsrc/Tools/Spec_Check/Spec_Check.thy
The file was addedsrc/Tools/Spec_Check/base_generator.ML
The file was addedsrc/Tools/Spec_Check/gen_construction.ML
The file was addedsrc/Tools/Spec_Check/generator.ML
The file was addedsrc/Tools/Spec_Check/output_style.ML
The file was addedsrc/Tools/Spec_Check/property.ML
The file was addedsrc/Tools/Spec_Check/random.ML
The file was addedsrc/Tools/Spec_Check/spec_check.ML
The file was modified src/Tools/ROOT
Changeset 74188:ea10e06adede by wenzelm:
more Isabelle/Haskell operations;
The file was modified src/Tools/Haskell/Haskell.thy
Changeset 74187:6109a9105a7a by wenzelm:
more Isabelle/Haskell operations;
The file was modified src/Tools/Haskell/Haskell.thy
Changeset 74186:92e74f9305a4 by wenzelm:
more Isabelle/Haskell operations;
The file was modified src/Tools/Haskell/Haskell.thy
Changeset 74185:2508ea6a9a11 by wenzelm:
more Isabelle/Haskell operations;
The file was modified src/Tools/Haskell/Haskell.thy
Changeset 74184:7652f8d29d10 by wenzelm:
clarified signature;
The file was modified src/Tools/Haskell/Haskell.thy
Changeset 74183:af81e4a307be by wenzelm:
clarified signature;
The file was modified src/Pure/General/name_space.ML
The file was modified src/Pure/General/position.ML
The file was modified src/Pure/Isar/calculation.ML
The file was modified src/Pure/Isar/keyword.ML
The file was modified src/Pure/Isar/outer_syntax.ML
The file was modified src/Pure/PIDE/resources.ML
The file was modified src/Pure/Syntax/syntax_phases.ML
The file was modified src/Pure/theory.ML
Changeset 74182:72bb7e9143f7 by wenzelm:
minor performance tuning;
The file was modified src/Pure/General/position.ML
The file was modified src/Pure/PIDE/markup.ML
The file was modified src/Pure/PIDE/markup.scala
The file was modified src/Tools/Haskell/Haskell.thy
Changeset 74181:4ae14c2e7cdd by wenzelm:
tuned;
The file was modified src/Pure/General/position.ML
Changeset 74180:5d40a4f66fdd by wenzelm:
tuned;
The file was modified src/Pure/General/position.ML
Changeset 74179:54e096758b63 by wenzelm:
tuned signature;
The file was modified src/Pure/General/position.ML
Changeset 74178:5f81ebfb551e by wenzelm:
tuned comments;
The file was modified src/Tools/Haskell/Haskell.thy
Changeset 74177:a8b032dede5c by wenzelm:
treat Symbol.eof as in ML (but: presently unused);
The file was modified src/Tools/Haskell/Haskell.thy
Changeset 74176:b70714530045 by wenzelm:
tuned;
The file was modified src/Pure/General/position.ML
The file was modified src/Tools/Haskell/Haskell.thy
Changeset 74175:53e28c438f96 by wenzelm:
minor performance tuning;
The file was modified src/Pure/General/symbol_pos.ML
The file was modified src/Pure/Isar/token.ML
Changeset 74174:a3b0fc510705 by wenzelm:
clarified signature;
The file was modified src/HOL/SPARK/Tools/fdl_lexer.ML
The file was modified src/Pure/General/position.ML
The file was modified src/Pure/General/symbol_pos.ML
The file was modified src/Pure/Isar/token.ML
The file was modified src/Pure/ML/ml_lex.ML
The file was modified src/Pure/Pure.thy
The file was modified src/Tools/Haskell/Haskell.thy
Changeset 74173:8d03d548df1c by wenzelm:
proper Isabelle symbol positions;
The file was modified src/Tools/Haskell/Haskell.thy
Changeset 74172:c576a4e2ffbc by wenzelm:
more Haskell operations;
The file was modified src/Tools/Haskell/Haskell.thy
Changeset 74171:a9e79c3645c4 by wenzelm:
clarified signature;
The file was modified src/HOL/SPARK/Tools/fdl_lexer.ML
The file was modified src/Pure/General/position.ML
The file was modified src/Pure/General/symbol_pos.ML
The file was modified src/Pure/Isar/token.ML
The file was modified src/Pure/ML/ml_lex.ML
The file was modified src/Pure/Pure.thy
Changeset 74170:09d4175f473e by wenzelm:
tuned;
The file was modified src/Pure/General/symbol_explode.ML
Changeset 74169:43fe7388458f by wenzelm:
tuned;
The file was modified src/Tools/Haskell/Haskell.thy
Changeset 74168:f0b2136e2204 by wenzelm:
tuned signature: prefer existing Haskell operations;
The file was modified src/Tools/Haskell/Haskell.thy
Changeset 74167:25c672c32467 by wenzelm:
more Haskell operations;
The file was modified src/Tools/Haskell/Haskell.thy
Changeset 74166:ff3dbb2be924 by wenzelm:
tuned signature;
The file was modified src/Pure/Concurrent/future.ML
The file was modified src/Pure/General/position.ML
The file was modified src/Pure/PIDE/command.ML
The file was modified src/Pure/PIDE/document.ML
The file was modified src/Pure/Thy/export.ML
Changeset 74165:86163ea20e77 by wenzelm:
tuned comments;
The file was modified src/Pure/General/position.ML
Changeset 74164:7b93dc3f2b34 by wenzelm:
tuned;
The file was modified src/Pure/ML/ml_antiquotations2.ML
Changeset 74163:afe3c8ae1624 by haftmann:
consolidation of rules for bit operations
The file was modified NEWS
The file was modified src/HOL/Bit_Operations.thy
The file was modified src/HOL/Library/Word.thy

Summary

  1. Graphic rendering of Relational_Method PDF files refined.
  2. Entry Relational_Method updated.
  3. more realistic timeout;
  4. clarified signature;
  5. follow Isabelle/53e28c438f96;
  6. clarified signature, following Isabelle/a3b0fc510705;
  7. merged
  8. tuned
  9. consolidation of rules for bit operations
Changeset 11990:80d141ead0ab by Pasquale Noce _pasquale.noce@hidglobal.com_:
Graphic rendering of Relational_Method PDF files refined.
The file was modified thys/Relational_Method/Authentication.thy
Changeset 11989:5fa903cd1a85 by Pasquale Noce _pasquale.noce@hidglobal.com_:
Entry Relational_Method updated.
The file was modified thys/Relational_Method/Anonymity.thy
The file was modified thys/Relational_Method/Authentication.thy
The file was modified thys/Relational_Method/Definitions.thy
The file was modified thys/Relational_Method/Possibility.thy
Changeset 11988:0320f17157ee by wenzelm:
more realistic timeout;
The file was modified thys/CoCon/ROOT
The file was modified thys/CoSMeDis/ROOT
Changeset 11987:d5bc84fd503c by wenzelm:
clarified signature;
The file was modified thys/Isabelle_C/C11-FrontEnd/src/C_Lexer_Annotation.thy
The file was modified thys/Isabelle_C/C11-FrontEnd/src/C_Parser_Annotation.thy
The file was modified thys/Isabelle_C/C11-FrontEnd/src/C_Parser_Language.thy
Changeset 11986:f1bf23e16821 by wenzelm:
follow Isabelle/53e28c438f96;
The file was modified thys/Isabelle_C/C11-FrontEnd/src/C_Lexer_Annotation.thy
Changeset 11985:e3caeb84ccd9 by wenzelm:
clarified signature, following Isabelle/a3b0fc510705;
The file was modified thys/Isabelle_C/C11-FrontEnd/src/C_Lexer_Annotation.thy
The file was modified thys/Isabelle_C/C11-FrontEnd/src/C_Lexer_Language.thy
Changeset 11984:7bd41cfb12ad by nipkow:
merged
Changeset 11983:376d3a9f6285 by nipkow:
tuned
The file was modified thys/Approximation_Algorithms/Center_Selection.thy
Changeset 11982:897dc683c2ec by haftmann:
consolidation of rules for bit operations
The file was modified thys/Native_Word/Code_Symbolic_Bits_Int.thy
The file was modified thys/Word_Lib/Examples.thy
The file was modified thys/Word_Lib/Legacy_Aliases.thy
The file was modified thys/Word_Lib/More_Word.thy
The file was modified thys/Word_Lib/More_Word_Operations.thy