equal
deleted
inserted
replaced
15 "A Comparison of HOL-ST and Isabelle/ZF" by Sten Agerholm |
15 "A Comparison of HOL-ST and Isabelle/ZF" by Sten Agerholm |
16 Technical Report No. 369, University of Cambridge Computer |
16 Technical Report No. 369, University of Cambridge Computer |
17 Laboratory, 1995. |
17 Laboratory, 1995. |
18 *) |
18 *) |
19 |
19 |
20 theory Limit imports Main begin |
20 theory Limit imports ZF begin |
21 |
21 |
22 definition |
22 definition |
23 rel :: "[i,i,i]=>o" where |
23 rel :: "[i,i,i]=>o" where |
24 "rel(D,x,y) == <x,y>:snd(D)" |
24 "rel(D,x,y) == <x,y>:snd(D)" |
25 |
25 |