| author | nipkow |
| Thu, 11 Nov 1999 12:23:45 +0100 | |
| changeset 8011 | d14c4e9e9c8e |
| child 8116 | 759f712f8f06 |
| permissions | -rw-r--r-- |
1 (* Title: HOL/MicroJava/J/JBasis.thy
2 ID: $Id$
3 Author: David von Oheimb
4 Copyright 1999 TU Muenchen
6 Some auxiliary definitions.
7 *)
9 JBasis = Main +
11 constdefs
13 unique :: "('a \\<times> 'b) list \\<Rightarrow> bool"
14 "unique \\<equiv> nodups \\<circ> map fst"
16 list_all2 :: "('a \\<Rightarrow> 'b \\<Rightarrow> bool) \\<Rightarrow> ('a list \\<Rightarrow> 'b list \\<Rightarrow> bool)"
17 "list_all2 P xs ys \\<equiv> length xs = length ys \\<and> (\\<forall> (x,y)\\<in>set (zip xs ys). P x y)"
19 end