| changeset 42463 | f270e3e18be5 |
| parent 41460 | ea56b98aee83 |
| child 44367 | 74c08021ab2e |
--- a/src/HOL/ex/Unification.thy Fri Apr 22 15:57:43 2011 +0200 +++ b/src/HOL/ex/Unification.thy Sat Apr 23 13:00:19 2011 +0200 @@ -31,8 +31,7 @@ | Const 'a | App "'a trm" "'a trm" (infix "\<cdot>" 60) -types - 'a subst = "('a \<times> 'a trm) list" +type_synonym 'a subst = "('a \<times> 'a trm) list" text {* Applying a substitution to a variable: *}