changeset 149 | e122cb146ecc |
parent 31 | b6815473ee2e |
child 162 | e93760534354 |
148:3b7477db3462 | 149:e122cb146ecc |
---|---|
1 theory Prefix_subtract |
1 theory Prefix_subtract |
2 imports Main List_Prefix |
2 imports Main |
3 "~~/src/HOL/Library/List_Prefix" |
|
3 begin |
4 begin |
4 |
5 |
5 section {* A small theory of prefix subtraction *} |
6 section {* A small theory of prefix subtraction *} |
6 |
7 |
7 text {* |
8 text {* |