author | haftmann |
Tue, 23 Sep 2008 18:11:44 +0200 | |
changeset 28337 | 93964076e7b8 |
parent 28263 | 69eaa97e7e96 |
child 28952 | 15a4b2cf8c34 |
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 |
|
27368 | 4 |
Classical Higher-order Logic -- batteries included. |
923 | 5 |
*) |
6 |
||
27421 | 7 |
use_thy "Complex/Complex_Main"; |
28263 | 8 |
|
9 |
val HOL_proofs = ! Proofterm.proofs; |
|
10 |