theory Peter
imports Main
begin

types t = "string"
types indexed_orders = "nat \<Rightarrow> (t*t) set"

constdefs
mytest :: "indexed_orders \<Rightarrow> nat \<Rightarrow> t \<Rightarrow> t \<Rightarrow> bool"
"mytest tos n t1 t2 == (t1,t2) \<in> tos n"

abbreviation
  in_rel :: "'a \<Rightarrow> ('a * 'b) set \<Rightarrow> 'b \<Rightarrow> bool" ("(_/ \<le>\<^bsub>_\<^esub> _)" [51, 0, 51] 50) where
  "x \<le>\<^bsub>R\<^esub> y \<equiv> (x, y) \<in> R"

text {*
The definition of @{text mytest} is
@{thm [display] mytest_def [no_vars]}
The introduction rule @{text rtrancl_into_rtrancl} for the transitive closure is
@{thm [display] rtrancl_into_rtrancl [no_vars]}
*}

end