equal
deleted
inserted
replaced
16 no_document time_use_thy "Pretty_Int"; |
16 no_document time_use_thy "Pretty_Int"; |
17 time_use_thy "Random"; |
17 time_use_thy "Random"; |
18 |
18 |
19 no_document time_use_thy "Executable_Rat"; |
19 no_document time_use_thy "Executable_Rat"; |
20 no_document time_use_thy "Efficient_Nat"; |
20 no_document time_use_thy "Efficient_Nat"; |
21 time_use_thy "Codegenerator_Rat"; |
|
22 no_document time_use_thy "Codegenerator"; |
21 no_document time_use_thy "Codegenerator"; |
|
22 no_document time_use_thy "Codegenerator_Pretty"; |
23 |
23 |
24 time_use_thy "Higher_Order_Logic"; |
24 time_use_thy "Higher_Order_Logic"; |
25 time_use_thy "Abstract_NAT"; |
25 time_use_thy "Abstract_NAT"; |
26 time_use_thy "Guess"; |
26 time_use_thy "Guess"; |
27 time_use_thy "Binary"; |
27 time_use_thy "Binary"; |