| changeset 9336 | 9ae89b9ce206 |
| parent 9109 | 0085c32a533b |
| child 10265 | 4e004b548049 |
--- a/src/HOL/UNITY/AllocBase.thy Fri Jul 14 14:46:35 2000 +0200 +++ b/src/HOL/UNITY/AllocBase.thy Fri Jul 14 14:47:15 2000 +0200 @@ -24,10 +24,6 @@ "tokens [] = 0" "tokens (x#xs) = x + tokens xs" -constdefs sublist :: "['a list, nat set] => 'a list" - "sublist l A == map fst (filter (%p. snd p : A) (zip l [0..size l(]))" - - consts bag_of :: 'a list => 'a multiset