src/HOL/ROOT.ML
author wenzelm
Thu, 15 May 2008 17:39:20 +0200
changeset 26902 8db1e960d636
parent 25964 080f89d89990
child 27368 9f90ac19e32b
permissions -rw-r--r--
updated generated file;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1264
3eb91524b938 added local simpsets; removed IOA from 'make test'
clasohm
parents: 1165
diff changeset
     1
(*  Title:      HOL/ROOT.ML
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     2
    ID:         $Id$
23166
45f3c90b2d27 proper loading of ML files (in HOL.thy);
wenzelm
parents: 22997
diff changeset
     3
 
7739
bfe45b716dfc tuned comment;
wenzelm
parents: 7703
diff changeset
     4
Classical Higher-order Logic.
923
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     5
*)
ff1574a81019 new version of HOL with curried function application
clasohm
parents:
diff changeset
     6
23166
45f3c90b2d27 proper loading of ML files (in HOL.thy);
wenzelm
parents: 22997
diff changeset
     7
use_thy "Main";