equal
deleted
inserted
replaced
7 |
7 |
8 theory HOL_Light_Import |
8 theory HOL_Light_Import |
9 imports HOL_Light_Maps |
9 imports HOL_Light_Maps |
10 begin |
10 begin |
11 |
11 |
12 import_file "$HOL_LIGHT_DUMP" |
12 import_file "$HOL_LIGHT_BUNDLE" |
13 |
13 |
14 end |
14 end |
15 |
15 |