changeset 28228 | 7ebe8dc06cbb |
parent 28109 | 3f76ae637f71 |
child 28243 | 84d90ec67059 |
28227:77221ee0f7b9 | 28228:7ebe8dc06cbb |
---|---|
4 Miscellaneous examples for Higher-Order Logic. |
4 Miscellaneous examples for Higher-Order Logic. |
5 *) |
5 *) |
6 |
6 |
7 no_document use_thys [ |
7 no_document use_thys [ |
8 "Parity", |
8 "Parity", |
9 "Eval", |
9 "Code_Eval", |
10 "State_Monad", |
10 "State_Monad", |
11 "Efficient_Nat_examples", |
11 "Efficient_Nat_examples", |
12 "ExecutableContent", |
12 "ExecutableContent", |
13 "FuncSet", |
13 "FuncSet", |
14 "Word", |
14 "Word", |