| changeset 542 | 4b96e3c8b33e |
| parent 539 | 12861a362099 |
| child 550 | 95d6853dec4a |
| 541:96d10631eec2 | 542:4b96e3c8b33e |
|---|---|
697 section {* Concurrency (TBD) *} |
697 section {* Concurrency (TBD) *} |
698 |
698 |
699 text {* |
699 text {* |
700 @{ML_ind prove_future in Goal} |
700 @{ML_ind prove_future in Goal} |
701 @{ML_ind future_result in Goal} |
701 @{ML_ind future_result in Goal} |
702 @{ML_ind fork_pri in Future} |
|
703 *} |
702 *} |
704 |
703 |
705 section {* Parse and Print Translations (TBD) *} |
704 section {* Parse and Print Translations (TBD) *} |
706 |
705 |
707 section {* Summary *} |
706 section {* Summary *} |