equal
deleted
inserted
replaced
1 (* Title: HOL/ex/Efficient_Nat_examples.thy |
1 (* Title: HOL/ex/Efficient_Nat_examples.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Florian Haftmann, TU Muenchen |
3 Author: Florian Haftmann, TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 header {* Simple examples for Efficient\_Nat theory. *} |
6 header {* Simple examples for Efficient\_Nat theory. *} |
7 |
7 |
8 theory Efficient_Nat_examples |
8 theory Efficient_Nat_examples |
9 imports Main "~~/src/HOL/Real/RealDef" Efficient_Nat |
9 imports Main "~~/src/HOL/Real/RealDef" Efficient_Nat |
10 begin |
10 begin |
11 |
11 |