Skip to content

Commit

Permalink
update README.md
Browse files Browse the repository at this point in the history
  • Loading branch information
@fblanqui
fblanqui committed Oct 12, 2023
1 parent 47e5caf commit 2a24cbd
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -105,9 +105,10 @@ Generating dk/lp files from dumped files

The base theory in which HOL-Light proofs are translated is described in the files [theory_hol.lp](https://github.com/Deducteam/hol2dk/blob/main/theory_hol.lp) and [theory_hol.dk](https://github.com/Deducteam/hol2dk/blob/main/theory_hol.dk).

You first need to generate `file.pos` with:
You first need to generate `file.pos` and `file.use` with:
```
hol2dk pos file
hol2dk use file
```

You can then generate `file.dk` with:
Expand Down

0 comments on commit 2a24cbd

Please sign in to comment.