equal
deleted
inserted
replaced
|
1 (* Title: HOL/Main.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 Copyright 2000 TU Muenchen |
1 |
5 |
2 (*theory Main includes everything; note that theory |
6 Theory Main includes everything. |
3 PreList already includes most HOL theories*) |
7 Note that theory PreList already includes most HOL theories. |
|
8 *) |
4 |
9 |
5 theory Main = Map + String: |
10 theory Main = Map + String: |
6 |
11 |
7 (*belongs to theory List*) |
12 (*belongs to theory List*) |
8 declare lists_mono [mono] |
13 declare lists_mono [mono] |