changeset 17466 | 92d36be64b46 |
parent 17413 | 89ccb3799428 |
child 17505 | 928bd7053d6a |
17465:93fc1211603f | 17466:92d36be64b46 |
---|---|
49 time_use_thy "Quickcheck_Examples"; |
49 time_use_thy "Quickcheck_Examples"; |
50 |
50 |
51 no_document use_thy "Word"; |
51 no_document use_thy "Word"; |
52 time_use_thy "Adder"; |
52 time_use_thy "Adder"; |
53 |
53 |
54 no_document time_use_thy "Hebrew"; |
54 HTML.with_charset "utf-8" (no_document time_use_thy) "Hebrew"; |