author | haftmann |
Tue, 10 Jul 2007 17:30:50 +0200 | |
changeset 23709 | fd31da8f752a |
parent 23166 | 45f3c90b2d27 |
child 23894 | 1a4167d761ac |
permissions | -rw-r--r-- |
1264
3eb91524b938
added local simpsets; removed IOA from 'make test'
clasohm
parents:
1165
diff
changeset
|
1 |
(* Title: HOL/ROOT.ML |
923 | 2 |
ID: $Id$ |
23166 | 3 |
|
7739 | 4 |
Classical Higher-order Logic. |
923 | 5 |
*) |
6 |
||
23166 | 7 |
use_thy "Main"; |
10275 | 8 |
|
10263 | 9 |
path_add "~~/src/HOL/Library"; |
5124 | 10 |
|
5501 | 11 |
Goal "True"; (*leave subgoal package empty*) |