Renamed accessible part for predicates to accp.
authorberghofe
Wed Jul 11 11:54:03 2007 +0200 (2007-07-11)
changeset 2377760b7800338d5
parent 23776 2215169c93fa
child 23778 18f426a137a9
Renamed accessible part for predicates to accp.
src/HOL/ex/Unification.thy
     1.1 --- a/src/HOL/ex/Unification.thy	Wed Jul 11 11:52:45 2007 +0200
     1.2 +++ b/src/HOL/ex/Unification.thy	Wed Jul 11 11:54:03 2007 +0200
     1.3 @@ -458,7 +458,7 @@
     1.4  
     1.5    from `unify_dom (M \<cdot> N, M' \<cdot> N')`
     1.6    have "unify_dom (M, M')"
     1.7 -    by (rule acc_downward) (rule unify_rel.intros)
     1.8 +    by (rule accp_downward) (rule unify_rel.intros)
     1.9    hence no_new_vars: 
    1.10      "\<And>t. vars_of (t \<triangleleft> \<theta>1) \<subseteq> vars_of M \<union> vars_of M' \<union> vars_of t"
    1.11      by (rule unify_vars) (rule `unify M M' = Some \<theta>1`)