set "baseuri" "cic:/matita/CoRN-Decl/tactics/AlgReflection".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: AlgReflection.v,v 1.2 2004/03/26 16:07:03 lcf Exp $ *)
include "algebra/CLogic.ma".
(* UNEXPORTED
-Section Syntactic_Expressions.
+Section Syntactic_Expressions
*)
inline "cic:/CoRN/tactics/AlgReflection/varindex.con".
inline "cic:/CoRN/tactics/AlgReflection/expr_power.con".
(* UNEXPORTED
-End Syntactic_Expressions.
+End Syntactic_Expressions
*)
(* UNEXPORTED
-Section Normalization_Function.
+Section Normalization_Function
*)
inline "cic:/CoRN/tactics/AlgReflection/eq_nat.con".
inline "cic:/CoRN/tactics/AlgReflection/expr_is_zero.con".
(* UNEXPORTED
-End Normalization_Function.
+End Normalization_Function
*)
(* UNEXPORTED
-Section Correctness_Results.
+Section Correctness_Results
*)
inline "cic:/CoRN/tactics/AlgReflection/eq_nat_corr.con".
inline "cic:/CoRN/tactics/AlgReflection/eq_expr_corr.con".
(* UNEXPORTED
-End Correctness_Results.
+End Correctness_Results
*)
(* end hide *)