equal
deleted
inserted
replaced
2 (*theory Main includes everything; note that theory |
2 (*theory Main includes everything; note that theory |
3 PreList already includes most HOL theories*) |
3 PreList already includes most HOL theories*) |
4 |
4 |
5 theory Main = Map + String: |
5 theory Main = Map + String: |
6 |
6 |
7 (*actually belongs to theory List*) |
7 (*belongs to theory List*) |
8 lemmas [mono] = lists_mono |
8 declare lists_mono [mono] |
9 lemmas [recdef_cong] = map_cong |
9 declare map_cong [recdef_cong] |
10 |
10 |
11 end |
11 end |