# HG changeset patch
# User krauss
# Date 1313957584 -7200
# Node ID 7321d628b57d4a3cbacda26f0b47b1f65e197ce0
# Parent  f9825056dbabfc4c477896eadc03a5373b806e16
removed technical or trivial unused facts

diff -r f9825056dbab -r 7321d628b57d src/HOL/ex/Unification.thy
--- a/src/HOL/ex/Unification.thy	Sun Aug 21 22:13:04 2011 +0200
+++ b/src/HOL/ex/Unification.thy	Sun Aug 21 22:13:04 2011 +0200
@@ -53,9 +53,6 @@
 lemma finite_vars_of[intro]: "finite (vars_of t)"
   by (induct t) simp_all
 
-lemma vars_var_iff: "v \<in> vars_of (Var w) \<longleftrightarrow> w = v"
-  by auto
-
 lemma vars_iff_occseq: "x \<in> vars_of t \<longleftrightarrow> Var x \<prec> t \<or> Var x = t"
   by (induct t) auto
 
@@ -99,10 +96,6 @@
 lemma repl_invariance: "v \<notin> vars_of t \<Longrightarrow> t \<lhd> (v,u) # s = t \<lhd> s"
 by (simp add: agreement)
 
-lemma Var_in_subst:
-  "v \<in> vars_of t \<Longrightarrow> w \<in> vars_of (t \<lhd> (v, Var(w)) # s)"
-by (induct t) auto
-
 lemma remove_var: "v \<notin> vars_of s \<Longrightarrow> v \<notin> vars_of (t \<lhd> [(v, s)])"
 by (induct t) simp_all