src/HOL/plain.ML
author ballarin
Fri, 19 Dec 2008 16:39:23 +0100
changeset 29249 4dc278c8dc59
parent 29234 60f7fb56f8cd
child 29304 5c71a6da989d
permissions -rw-r--r--
All logics ported to new locales.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
27368
9f90ac19e32b established Plain theory and image
haftmann
parents:
diff changeset
     1
(*  Title:      HOL/plain.ML
9f90ac19e32b established Plain theory and image
haftmann
parents:
diff changeset
     2
 
9f90ac19e32b established Plain theory and image
haftmann
parents:
diff changeset
     3
Classical Higher-order Logic -- plain Tool bootstrap.
9f90ac19e32b established Plain theory and image
haftmann
parents:
diff changeset
     4
*)
9f90ac19e32b established Plain theory and image
haftmann
parents:
diff changeset
     5
9f90ac19e32b established Plain theory and image
haftmann
parents:
diff changeset
     6
use_thy "Plain";