| author | sultana |
| Tue, 24 Apr 2012 13:59:29 +0100 | |
| changeset 47730 | 15f4309bb9eb |
| parent 47266 | bf9796e44584 |
| permissions | -rw-r--r-- |
|
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
1 |
use_thy "HOL_Light_Maps"; |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
2 |
|
|
47266
bf9796e44584
clarified terminology; added reference to bundle component
krauss
parents:
47258
diff
changeset
|
3 |
if getenv "HOL_LIGHT_BUNDLE" <> "" |
|
47258
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
4 |
then use_thy "HOL_Light_Import" |
|
880e587eee9f
Modernized HOL-Import for HOL Light
Cezary Kaliszyk <cezarykaliszyk@gmail.com>
parents:
diff
changeset
|
5 |
else () |