equal
deleted
inserted
replaced
1 (* Title: HOL/ex/ROOT.ML |
1 (* Title: HOL/ex/ROOT.ML |
2 ID: $Id$ |
|
3 |
2 |
4 Miscellaneous examples for Higher-Order Logic. |
3 Miscellaneous examples for Higher-Order Logic. |
5 *) |
4 *) |
6 |
5 |
7 no_document use_thys [ |
6 no_document use_thys [ |
8 "Parity", |
|
9 "Code_Eval", |
|
10 "State_Monad", |
7 "State_Monad", |
11 "Efficient_Nat_examples", |
8 "Efficient_Nat_examples", |
12 "ExecutableContent", |
9 "ExecutableContent", |
13 "FuncSet", |
10 "FuncSet", |
14 "Word", |
11 "Word", |
99 "../NumberTheory/Factorization", |
96 "../NumberTheory/Factorization", |
100 "../Library/BigO" |
97 "../Library/BigO" |
101 ]; |
98 ]; |
102 |
99 |
103 use_thys [ |
100 use_thys [ |
104 "../Complex/ex/BinEx", |
101 "BinEx", |
105 "../Complex/ex/Sqrt", |
102 "Sqrt", |
106 "../Complex/ex/Sqrt_Script", |
103 "Sqrt_Script", |
107 "../Complex/ex/BigO_Complex", |
104 "BigO_Complex", |
108 |
105 |
109 "../Complex/ex/Arithmetic_Series_Complex", |
106 "Arithmetic_Series_Complex", |
110 "../Complex/ex/HarmonicSeries", |
107 "HarmonicSeries", |
111 |
108 |
112 "../Complex/ex/MIR", |
109 "MIR", |
113 "../Complex/ex/ReflectedFerrack" |
110 "ReflectedFerrack" |
114 ]; |
111 ]; |
115 |
112 |