src/HOL/Subst/AList.thy
changeset 3192 a75558a4ed37
parent 1476 608483c2122a
child 3268 012c43174664
     1.1 --- a/src/HOL/Subst/AList.thy	Thu May 15 12:29:59 1997 +0200
     1.2 +++ b/src/HOL/Subst/AList.thy	Thu May 15 12:40:01 1997 +0200
     1.3 @@ -12,7 +12,7 @@
     1.4    alist_rec  :: "[('a*'b)list, 'c, ['a, 'b, ('a*'b)list, 'c]=>'c] => 'c"
     1.5    assoc      :: "['a,'b,('a*'b) list] => 'b"
     1.6  
     1.7 -rules
     1.8 +defs
     1.9  
    1.10    alist_rec_def "alist_rec al b c == list_rec b (split c) al"
    1.11