author | wenzelm |
Sat, 07 Apr 2012 16:41:59 +0200 | |
changeset 47389 | e8552cba702d |
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 () |