OCaml e Hol-Light

[hubabuba]

Salve a tutti.
Sono nuova alla programmazione 0Caml e Hol-Light.Il programma non mi riconosce questo comando INTRO_TAC. Ce qualcuno che mi può dare una mano? Grazie

[hamming_burst]

Ciao,
uuh theorem prover...

Penso ti riferisca ad un comando proprio di Hol (che non conosco direttamente) che non è riconosciuto e non ad uno di O'Caml, giusto?

[apatriarca]

Condivido la perplessità di hamming_burst. Dovresti fornirci maggiori informazioni. Le ragioni potrebbero in effetti essere principalmente due:
1. hai scritto il codice sbagliato, ma non abbiamo modo di verificarlo in alcun modo;
2. non hai installato correttamente O'Caml e/o Hol-Light.
In nessuno dei due casi possiamo dire qualcosa con le poche informazioni che ci hai fornito.

[hubabuba]

Avete pienamente ragione. Questo è un comando che è stato creato dal nostro prof. Però funziona solo nei laboratori del'università. Quindi mi serve il file.ml per far funzionare questo comando. Grazie