equal
deleted
inserted
replaced
3 Miscellaneous examples for Higher-Order Logic. |
3 Miscellaneous examples for Higher-Order Logic. |
4 *) |
4 *) |
5 |
5 |
6 no_document use_thys [ |
6 no_document use_thys [ |
7 "~~/src/HOL/Library/State_Monad", |
7 "~~/src/HOL/Library/State_Monad", |
8 "Efficient_Nat_examples", |
8 "Code_Nat_examples", |
9 "~~/src/HOL/Library/FuncSet", |
9 "~~/src/HOL/Library/FuncSet", |
10 "Eval_Examples", |
10 "Eval_Examples", |
11 "Normalization_by_Evaluation", |
11 "Normalization_by_Evaluation", |
12 "Hebrew", |
12 "Hebrew", |
13 "Chinese", |
13 "Chinese", |