equal
deleted
inserted
replaced
1 (* Title: LK/LK0.thy |
1 (* Title: Sequents/LK0.thy |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Copyright 1993 University of Cambridge |
3 Copyright 1993 University of Cambridge |
4 |
4 |
5 There may be printing problems if a seqent is in expanded normal form |
5 There may be printing problems if a seqent is in expanded normal form |
6 (eta-expanded, beta-contracted). |
6 (eta-expanded, beta-contracted). |