[isabelle] weird message about Proof may be skipped in quick_and_dirty mode only!
Trying to load the HOL source files I get the following error
- with_path "Integ" use_thy "Main";
Loading theory "Product_Type" (required by "Main" ...)
### Unnamed infix operator "*" -- deprecated
*** Proof may be skipped in quick_and_dirty mode only!
*** At command "typedef" (line 16 of
! Uncaught exception:
I get the error regardless of whether I have set quick_and_dirty or not
- quick_and_dirty ;
> val it = ref true : bool ref
Thanks for any help
This archive was generated by a fusion of
Pipermail (Mailman edition) and