changeset 5976 | 44290b71a85f |
parent 4559 | 8e604d885b54 |
child 6340 | 7d5cbd5819a0 |
5975:cd19eaa90f45 | 5976:44290b71a85f |
---|---|
1 (* Title: HOLCF/IOA/meta_theory/TLS.thy |
1 (* Title: HOLCF/IOA/meta_theory/Pred.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Olaf M"uller |
3 Author: Olaf M"uller |
4 Copyright 1997 TU Muenchen |
4 Copyright 1997 TU Muenchen |
5 |
5 |
6 Logical Connectives lifted to predicates. |
6 Logical Connectives lifted to predicates. |
7 |
|
8 ToDo: |
|
9 |
|
10 <--> einfuehren. |
|
11 |
7 |
12 *) |
8 *) |
13 |
9 |
14 Pred = Arith + |
10 Pred = Arith + |
15 |
11 |