equal
deleted
inserted
replaced
1 * Compile and run "offline/offline.ml" (warning, this uses a lot of memory) |
|
2 |
|
3 ocamlopt offline.ml -o offline |
|
4 > maps.lst |
|
5 ./offline |
|
6 |
|
7 * Format of maps.lst: |
|
8 |
|
9 - THM1 THM2 map HOL Light THM1 to Isabelle/HOL THM2 and forget its deps |
|
10 - THM - do not record THM and make sure it is not used (its deps must be mapped) |
|
11 - THM the definition of constant/type is mapped in Isabelle/HOL, so forget |
|
12 its deps and look its map up when defining (may fail at import time) |
|