removed technical or trivial unused facts
authorkrauss
Sun Aug 21 22:13:04 2011 +0200 (2011-08-21)
changeset 443737321d628b57d
parent 44372 f9825056dbab
child 44374 0b217404522a
removed technical or trivial unused facts
src/HOL/ex/Unification.thy
     1.1 --- a/src/HOL/ex/Unification.thy	Sun Aug 21 22:13:04 2011 +0200
     1.2 +++ b/src/HOL/ex/Unification.thy	Sun Aug 21 22:13:04 2011 +0200
     1.3 @@ -53,9 +53,6 @@
     1.4  lemma finite_vars_of[intro]: "finite (vars_of t)"
     1.5    by (induct t) simp_all
     1.6  
     1.7 -lemma vars_var_iff: "v \<in> vars_of (Var w) \<longleftrightarrow> w = v"
     1.8 -  by auto
     1.9 -
    1.10  lemma vars_iff_occseq: "x \<in> vars_of t \<longleftrightarrow> Var x \<prec> t \<or> Var x = t"
    1.11    by (induct t) auto
    1.12  
    1.13 @@ -99,10 +96,6 @@
    1.14  lemma repl_invariance: "v \<notin> vars_of t \<Longrightarrow> t \<lhd> (v,u) # s = t \<lhd> s"
    1.15  by (simp add: agreement)
    1.16  
    1.17 -lemma Var_in_subst:
    1.18 -  "v \<in> vars_of t \<Longrightarrow> w \<in> vars_of (t \<lhd> (v, Var(w)) # s)"
    1.19 -by (induct t) auto
    1.20 -
    1.21  lemma remove_var: "v \<notin> vars_of s \<Longrightarrow> v \<notin> vars_of (t \<lhd> [(v, s)])"
    1.22  by (induct t) simp_all
    1.23