equal
deleted
inserted
replaced
4 Copyright 2001 University of Cambridge |
4 Copyright 2001 University of Cambridge |
5 |
5 |
6 Auxiliary definitions needed in Priority.thy |
6 Auxiliary definitions needed in Priority.thy |
7 *) |
7 *) |
8 |
8 |
9 PriorityAux = Main + |
9 PriorityAux = Main + |
10 |
10 |
11 types vertex |
11 types vertex |
12 arities vertex::term |
12 arities vertex :: type |
13 |
13 |
14 constdefs |
14 constdefs |
15 (* symmetric closure: removes the orientation of a relation *) |
15 (* symmetric closure: removes the orientation of a relation *) |
16 symcl :: "(vertex*vertex)set=>(vertex*vertex)set" |
16 symcl :: "(vertex*vertex)set=>(vertex*vertex)set" |
17 "symcl r == r Un (r^-1)" |
17 "symcl r == r Un (r^-1)" |