Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. repaired whitespace accident from 2505cabfc515
  2. proper namespace for evaluators
  3. tuned
  4. more correct name resolving
  5. skip abstract constructors silently in datatype clauses of computations
  6. removed para about 'old_datatype' in docs
  7. old_datatype no longer exists (cf. 706b1cf7b76d);
  8. merged
  9. PIDE markup for Markdown items (which may consist of multiple paragraphs or lists);
  10. clarified terminology of "markdown_bullet";
  11. compile
  12. updated dependencies + compile
  13. moved 'realizers' into their own theory, now that they are decupled from the old datatype construction
  14. removed 'old_datatype' command
  15. don't test 'old_datatype', which is on its way out
  16. ported inductive realizer to new datatype package
  17. removed needless theorems
  18. store high-level 'size' equations
  19. avoid call to function that may throw an exception in error message
Changeset 67331:a8770603a269 by haftmann:
repaired whitespace accident from 2505cabfc515
The file was modified src/Pure/thm.ML (diff)
Changeset 67330:2505cabfc515 by haftmann:
proper namespace for evaluators
The file was modified src/HOL/Library/code_test.ML (diff)
The file was modified src/HOL/Tools/value_command.ML (diff)
The file was modified src/Pure/thm.ML (diff)
Changeset 67329:eabcd2e2bc9b by haftmann:
tuned
The file was modified src/HOL/Tools/simpdata.ML (diff)
Changeset 67328:5ca7bb565ea2 by haftmann:
more correct name resolving
The file was modified src/Tools/Code/code_runtime.ML (diff)
Changeset 67327:89be5a4f514b by haftmann:
skip abstract constructors silently in datatype clauses of computations
The file was modified src/Doc/Codegen/Computations.thy (diff)
The file was modified src/Tools/Code/code_runtime.ML (diff)
Changeset 67326:17fdb2c98083 by blanchet:
removed para about 'old_datatype' in docs
The file was modified src/Doc/Datatypes/Datatypes.thy (diff)
Changeset 67325:79260409a680 by wenzelm:
old_datatype no longer exists (cf. 706b1cf7b76d);
The file was modified src/Doc/Datatypes/Datatypes.thy (diff)
The file was modified src/Doc/Isar_Ref/HOL_Specific.thy (diff)
Changeset 67324:4c94ec0488c7 by wenzelm:
merged
Changeset 67323:d02208cefbdb by wenzelm:
PIDE markup for Markdown items (which may consist of multiple paragraphs or lists);
The file was modified src/Pure/PIDE/markup.ML (diff)
The file was modified src/Pure/PIDE/markup.scala (diff)
The file was modified src/Pure/PIDE/rendering.scala (diff)
The file was modified src/Pure/Thy/markdown.ML (diff)
The file was modified src/Tools/jEdit/src/jedit_rendering.scala (diff)
Changeset 67322:734a4e44b159 by wenzelm:
clarified terminology of "markdown_bullet";
The file was modified src/Pure/PIDE/markup.ML (diff)
The file was modified src/Pure/PIDE/markup.scala (diff)
The file was modified src/Pure/PIDE/rendering.scala (diff)
The file was modified src/Pure/Thy/markdown.ML (diff)
The file was modified src/Tools/VSCode/extension/package.json (diff)
The file was modified src/Tools/VSCode/extension/src/decorations.ts (diff)
The file was modified src/Tools/jEdit/etc/options (diff)
Changeset 67321:706b1cf7b76d by blanchet:
compile
The file was modified src/HOL/Nominal/nominal_datatype.ML (diff)
Changeset 67320:6afba546f0e5 by blanchet:
updated dependencies + compile
The file was modified src/HOL/Datatype_Examples/Compat.thy (diff)
The file was modified src/HOL/Proofs/Extraction/Euclid.thy (diff)
The file was modified src/HOL/Proofs/Extraction/Higman_Extraction.thy (diff)
The file was modified src/HOL/Proofs/Extraction/Pigeonhole.thy (diff)
The file was modified src/HOL/Proofs/Extraction/QuotRem.thy (diff)
The file was modified src/HOL/Proofs/Extraction/Warshall.thy (diff)
The file was modified src/HOL/Proofs/Lambda/WeakNorm.thy (diff)
The file was modified src/HOL/Tools/Old_Datatype/old_datatype.ML (diff)
Changeset 67319:07176d5b81d5 by blanchet:
moved 'realizers' into their own theory, now that they are decupled from the old datatype construction
The file was addedsrc/HOL/Library/Realizers.thy
The file was modified src/HOL/Library/Old_Datatype.thy (diff)
The file was modified src/HOL/ROOT (diff)
Changeset 67318:0ee38196509e by blanchet:
removed 'old_datatype' command
The file was modified src/HOL/Library/Old_Datatype.thy (diff)
The file was modified src/HOL/Tools/Old_Datatype/old_datatype.ML (diff)
Changeset 67317:15ea49331fc7 by blanchet:
don't test 'old_datatype', which is on its way out
The file was modified src/HOL/Datatype_Examples/Compat.thy (diff)
Changeset 67316:adaf279ce67b by blanchet:
ported inductive realizer to new datatype package
The file was modified src/HOL/Tools/inductive_realizer.ML (diff)
Changeset 67315:9301e197a47b by blanchet:
removed needless theorems
The file was modified src/HOL/Nominal/nominal_datatype.ML (diff)
Changeset 67314:315b5c29e927 by blanchet:
store high-level 'size' equations
The file was modified src/HOL/Tools/BNF/bnf_lfp_size.ML (diff)
Changeset 67313:a2d7c0987f19 by blanchet:
avoid call to function that may throw an exception in error message
The file was modified src/HOL/Tools/BNF/bnf_fp_rec_sugar_util.ML (diff)