Myhill_1.thy
changeset 149 e122cb146ecc
parent 110 e500cab16be4
child 162 e93760534354
equal deleted inserted replaced
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"