equal
deleted
inserted
replaced
1 quick_and_dirty := true; |
1 quick_and_dirty := true; |
2 |
2 |
3 no_document use_thys |
3 no_document use_thys |
4 ["Ex/ExLam", |
4 ["Ex/Lambda", |
5 "Ex/ExLF", |
5 "Ex/ExLF", |
6 "Ex/Ex1", |
6 "Ex/Ex1", |
7 "Ex/Ex1rec", |
7 "Ex/Ex1rec", |
8 "Ex/Ex2", |
8 "Ex/Ex2", |
9 "Ex/Ex3", |
9 "Ex/Ex3", |