| author | blanchet |
| Wed, 12 Sep 2012 17:26:05 +0200 | |
| changeset 49335 | 096967bf3940 |
| parent 47266 | bf9796e44584 |
| child 58889 | 5b7a9633cfa8 |
| permissions | -rw-r--r-- |
|
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
1 |
(* Title: HOL/Import/HOL_Light_Import.thy |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
2 |
Author: Cezary Kaliszyk, University of Innsbruck |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
3 |
Author: Alexander Krauss, QAware GmbH |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
4 |
*) |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
5 |
|
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
6 |
header {* Main HOL Light importer *}
|
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
7 |
|
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
8 |
theory HOL_Light_Import |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
9 |
imports HOL_Light_Maps |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
10 |
begin |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
11 |
|
|
47266
bf9796e44584
clarified terminology; added reference to bundle component
krauss
parents:
47258
diff
changeset
|
12 |
import_file "$HOL_LIGHT_BUNDLE" |
|
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
13 |
|
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
14 |
end |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
15 |