| author | blanchet |
| Mon, 21 May 2012 10:39:31 +0200 | |
| changeset 47944 | e6b51fab96f7 |
| 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 () |