[isabelle] Isabelle 2007 - Inductive sets + syntax



Hello,

I am wondering how I can change the following inductive set definition (along with its associated syntax) using Isabelle 2007. I am able to use the inductive_set syntax for its definition, however, I am unable to use the -e-> syntax.

consts
 eval :: "(B * bool)set"

syntax
 "_eval" :: "B => bool => bool" (infixl "-e->" 50)

translations
 "b -e-> b'" == "(b,b') : eval"

inductive eval
intros
TrueB: "TrueB -e-> True"
FalseB: "FalseB -e-> False"

TIA,

George





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