src/HOL/Bali/Table.thy
changeset 61069 aefe89038dd2
parent 58963 26bf09b95dda
child 62042 6c6ccf573479
     1.1 --- a/src/HOL/Bali/Table.thy	Mon Aug 31 20:56:24 2015 +0200
     1.2 +++ b/src/HOL/Bali/Table.thy	Mon Aug 31 21:01:21 2015 +0200
     1.3 @@ -361,7 +361,7 @@
     1.4  
     1.5  
     1.6  (*###TO Map?*)
     1.7 -primrec atleast_free :: "('a ~=> 'b) => nat => bool"
     1.8 +primrec atleast_free :: "('a \<rightharpoonup> 'b) => nat => bool"
     1.9  where
    1.10    "atleast_free m 0 = True"
    1.11  | atleast_free_Suc: "atleast_free m (Suc n) = (\<exists>a. m a = None & (!b. atleast_free (m(a|->b)) n))"