Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. old_datatype no longer exists (cf. 706b1cf7b76d);
  2. merged
  3. PIDE markup for Markdown items (which may consist of multiple paragraphs or lists);
  4. clarified terminology of "markdown_bullet";
  5. compile
  6. updated dependencies + compile
  7. moved 'realizers' into their own theory, now that they are decupled from the old datatype construction
  8. removed 'old_datatype' command
  9. don't test 'old_datatype', which is on its way out
  10. ported inductive realizer to new datatype package
  11. removed needless theorems
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)