equal
deleted
inserted
replaced
1 (* Title: HOL/HOLCF/FOCUS/Buffer_adm.thy |
1 (* Title: HOL/HOLCF/FOCUS/Buffer_adm.thy |
2 Author: David von Oheimb, TU Muenchen |
2 Author: David von Oheimb, TU Muenchen |
3 *) |
3 *) |
4 |
4 |
5 section {* One-element buffer, proof of Buf_Eq_imp_AC by induction + admissibility *} |
5 section \<open>One-element buffer, proof of Buf_Eq_imp_AC by induction + admissibility\<close> |
6 |
6 |
7 theory Buffer_adm |
7 theory Buffer_adm |
8 imports Buffer Stream_adm |
8 imports Buffer Stream_adm |
9 begin |
9 begin |
10 |
10 |