Theory RefRels

Up to index of Isabelle/HOL/Marvin2002

theory RefRels = HOL:

RefRels = HOL +

consts

refsto :: "['a, 'a] => bool" (infixl 42)
refeq  :: "['a, 'a] => bool" (infixl 42)

end