| author | wenzelm |
| Fri, 15 Aug 2008 15:50:52 +0200 | |
| changeset 27885 | 76b51cd0a37c |
| parent 25314 | 5eaf3e8b50a4 |
| child 28308 | d4396a28fb29 |
| permissions | -rw-r--r-- |
|
25314
5eaf3e8b50a4
moved stuff about size change termination to its own session
krauss
parents:
diff
changeset
|
1 |
(* Title: HOL/Matrix/ROOT.ML |
|
5eaf3e8b50a4
moved stuff about size change termination to its own session
krauss
parents:
diff
changeset
|
2 |
ID: $Id$ |
|
5eaf3e8b50a4
moved stuff about size change termination to its own session
krauss
parents:
diff
changeset
|
3 |
*) |
|
5eaf3e8b50a4
moved stuff about size change termination to its own session
krauss
parents:
diff
changeset
|
4 |
|
|
5eaf3e8b50a4
moved stuff about size change termination to its own session
krauss
parents:
diff
changeset
|
5 |
no_document use_thy "Infinite_Set"; |
|
5eaf3e8b50a4
moved stuff about size change termination to its own session
krauss
parents:
diff
changeset
|
6 |
no_document use_thy "Ramsey"; |
|
5eaf3e8b50a4
moved stuff about size change termination to its own session
krauss
parents:
diff
changeset
|
7 |
use_thy "Examples"; |