[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 "/home/users/jeremy/Isabelle2005/src/HOL/Product_Type.thy").
! Uncaught exception:
! ERROR

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

Jeremy





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.