Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] weird message about Proof may be skipped in qu...

Email Gateway (Aug 18 2022 at 09:43):

From: Jeremy Dawson <Jeremy.Dawson@rsise.anu.edu.au>
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

Last updated: May 03 2024 at 04:19 UTC