header {* Very Simple Predicate Logic with Equality *} theory VSPredEq imports VSPred begin consts "op =" :: "'a=> 'a=> o" (infix "=" 50) axioms refl: "x= x" sym: "x= y ==> y= x" trans: "[| x= y; y= z |] ==> x= z" cong: "x= y ==> f x= f y" subst: "[| x= y; P x |] ==> P y" end