changeset 149 | e122cb146ecc |
parent 110 | e500cab16be4 |
child 162 | e93760534354 |
148:3b7477db3462 | 149:e122cb146ecc |
---|---|
1 theory Myhill_1 |
1 theory Myhill_1 |
2 imports Main Folds While_Combinator |
2 imports Main Folds |
3 "~~/src/HOL/Library/While_Combinator" |
|
3 begin |
4 begin |
4 |
5 |
5 section {* Preliminary definitions *} |
6 section {* Preliminary definitions *} |
6 |
7 |
7 types lang = "string set" |
8 types lang = "string set" |