[isabelle] Isabelle 2007 - Inductive sets + syntax
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.
eval :: "(B * bool)set"
"_eval" :: "B => bool => bool" (infixl "-e->" 50)
"b -e-> b'" == "(b,b') : eval"
TrueB: "TrueB -e-> True"
FalseB: "FalseB -e-> False"
This archive was generated by a fusion of
Pipermail (Mailman edition) and