src/HOL/Prolog/ROOT.ML
author berghofe
Thu, 10 Oct 2002 14:21:49 +0200
changeset 13638 2b234b079245
parent 13208 965f95a3abd9
child 14981 e73f8140af78
permissions -rw-r--r--
Added choice_eq.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13208
965f95a3abd9 added the usual file headers
oheimb
parents: 9015
diff changeset
     1
(*  Title:    HOL/Prolog/ROOT.ML
965f95a3abd9 added the usual file headers
oheimb
parents: 9015
diff changeset
     2
    ID:       $Id$
965f95a3abd9 added the usual file headers
oheimb
parents: 9015
diff changeset
     3
    Author:   David von Oheimb (based on a lecture on Lambda Prolog by Nadathur)
965f95a3abd9 added the usual file headers
oheimb
parents: 9015
diff changeset
     4
    License:  GPL (GNU GENERAL PUBLIC LICENSE)
965f95a3abd9 added the usual file headers
oheimb
parents: 9015
diff changeset
     5
*)
965f95a3abd9 added the usual file headers
oheimb
parents: 9015
diff changeset
     6
9015
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
     7
use_thy"Test";
8006e9009621 added HOL/Prolog
oheimb
parents:
diff changeset
     8
use_thy"Type";