changeset 16417 | 9bc16273c2d4 |
parent 13612 | 55d32e76ef4e |
child 22808 | a7daa74e2980 |
16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
---|---|
3 Author: Ole Rasmussen |
3 Author: Ole Rasmussen |
4 Copyright 1995 University of Cambridge |
4 Copyright 1995 University of Cambridge |
5 Logic Image: ZF |
5 Logic Image: ZF |
6 *) |
6 *) |
7 |
7 |
8 theory Redex = Main: |
8 theory Redex imports Main begin |
9 consts |
9 consts |
10 redexes :: i |
10 redexes :: i |
11 |
11 |
12 datatype |
12 datatype |
13 "redexes" = Var ("n \<in> nat") |
13 "redexes" = Var ("n \<in> nat") |