equal
deleted
inserted
replaced
1 (* Title: ZF/Coind/Language.thy |
1 (* Title: ZF/Coind/Language.thy |
2 Author: Jacob Frost, Cambridge University Computer Laboratory |
2 Author: Jacob Frost, Cambridge University Computer Laboratory |
3 Copyright 1995 University of Cambridge |
3 Copyright 1995 University of Cambridge |
4 *) |
4 *) |
5 |
5 |
6 theory Language imports Main begin |
6 theory Language imports ZF begin |
7 |
7 |
8 |
8 |
9 text\<open>these really can't be definitions without losing the abstraction\<close> |
9 text\<open>these really can't be definitions without losing the abstraction\<close> |
10 |
10 |
11 axiomatization |
11 axiomatization |