
diff -r b1f486a9c56b -r f6da795ee27a src/HOL/Subst/UTerm.thy
--- a/src/HOL/Subst/UTerm.thy	Fri Apr 01 18:59:17 2005 +0200
+++ b/src/HOL/Subst/UTerm.thy	Fri Apr 01 21:04:00 2005 +0200
@@ -19,7 +19,10 @@
 consts
   vars_of  ::  "'a uterm => 'a set"
   "<:"     ::  "'a uterm => 'a uterm => bool"   (infixl 54) 
-uterm_size ::  "'a uterm => nat"
+  uterm_size ::  "'a uterm => nat"
+
+syntax (xsymbols)
+  "op <:"     ::  "'a uterm => 'a uterm => bool"   (infixl "\<prec>" 54) 
 
 
 primrec
@@ -27,11 +30,10 @@
   vars_of_Const: "vars_of (Const c) = {}"
   vars_of_Comb:  "vars_of (Comb M N) = (vars_of(M) Un vars_of(N))"
 
-
 primrec
-  occs_Var:   "u <: (Var v) = False"
-  occs_Const: "u <: (Const c) = False"
-  occs_Comb:  "u <: (Comb M N) = (u=M | u=N | u <: M | u <: N)"
+  occs_Var:   "u \<prec> (Var v) = False"
+  occs_Const: "u \<prec> (Const c) = False"
+  occs_Comb:  "u \<prec> (Comb M N) = (u=M | u=N | u \<prec> M | u \<prec> N)"
 
 primrec
   uterm_size_Var:   "uterm_size (Var v) = 0"
@@ -39,19 +41,20 @@
   uterm_size_Comb:  "uterm_size (Comb M N) = Suc(uterm_size M + uterm_size N)"
 
 
-lemma vars_var_iff: "(v : vars_of(Var(w))) = (w=v)"
+lemma vars_var_iff: "(v \<in> vars_of(Var(w))) = (w=v)"
 by auto
 
-lemma vars_iff_occseq: "(x : vars_of(t)) = (Var(x) <: t | Var(x) = t)"
+lemma vars_iff_occseq: "(x \<in> vars_of(t)) = (Var(x) \<prec> t | Var(x) = t)"
 by (induct_tac "t", auto)
 
 
-(* Not used, but perhaps useful in other proofs *)
-lemma occs_vars_subset: "M<:N --> vars_of(M) <= vars_of(N)"
+text{* Not used, but perhaps useful in other proofs *}
+lemma occs_vars_subset [rule_format]: "M\<prec>N --> vars_of(M) \<subseteq> vars_of(N)"
 by (induct_tac "N", auto)
 
 
-lemma monotone_vars_of: "vars_of M Un vars_of N <= (vars_of M Un A) Un (vars_of N Un B)"
+lemma monotone_vars_of:
+     "vars_of M Un vars_of N \<subseteq> (vars_of M Un A) Un (vars_of N Un B)"
 by blast
 
 lemma finite_vars_of: "finite(vars_of M)"




