set "baseuri" "cic:/matita/CoRN-Decl/tactics/RingReflection".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: RingReflection.v,v 1.4 2004/04/23 10:01:06 lcf Exp $ *)
inline "cic:/CoRN/tactics/RingReflection/pfun.var".
+(* NOTATION
+Notation II := (interpR R val unop binop pfun).
+*)
+
(*
four kinds of exprs: