equal
deleted
inserted
replaced
520 |
520 |
521 text {* |
521 text {* |
522 |
522 |
523 @{ML_response [display] "Sign.base_name \"List.list.Nil\"" "\"Nil\""} |
523 @{ML_response [display] "Sign.base_name \"List.list.Nil\"" "\"Nil\""} |
524 |
524 |
525 authentic syntax |
525 authentic syntax? |
|
526 |
|
527 *} |
|
528 |
|
529 ML {* @{const_name lfp} *} |
|
530 |
|
531 text {* |
|
532 constants in case-patterns? |
|
533 |
|
534 In the meantime, lfp has been moved to the Inductive theory, so it is |
|
535 no longer called Lfp.lfp. If a @{text "@{const_name}"} antiquotation had been |
|
536 used, we would have gotten an error for this. Another advantage of the |
|
537 antiquotation is that we can then just write @{text "@{const_name lfp}"} rather |
|
538 than @{text "@{const_name Lfp.lfp}"} or whatever, and it expands to the correct |
|
539 name. |
526 |
540 |
527 *} |
541 *} |
528 |
542 |
529 section {* Combinators\label{sec:combinators} *} |
543 section {* Combinators\label{sec:combinators} *} |
530 |
544 |
717 done |
731 done |
718 |
732 |
719 thm foo_def |
733 thm foo_def |
720 (*>*) |
734 (*>*) |
721 |
735 |
|
736 section {* Misc *} |
|
737 |
|
738 ML {*DatatypePackage.get_datatype @{theory} "List.list"*} |
|
739 |
722 end |
740 end |