src/HOL/W0/W0.thy
changeset 13890 90611b4e0054
parent 13601 fd3e3d6b37b2
child 14981 e73f8140af78
     1.1 --- a/src/HOL/W0/W0.thy	Tue Apr 01 16:08:34 2003 +0200
     1.2 +++ b/src/HOL/W0/W0.thy	Tue Apr 01 17:43:10 2003 +0200
     1.3 @@ -133,7 +133,7 @@
     1.4    by (rule ext) (simp add: id_subst_def)
     1.5  
     1.6  lemma dom_id_subst [simp]: "dom id_subst = {}"
     1.7 -  by (simp add: dom_def id_subst_def empty_def)
     1.8 +  by (simp add: dom_def id_subst_def)
     1.9  
    1.10  lemma cod_id_subst [simp]: "cod id_subst = {}"
    1.11    by (simp add: cod_def)