src/HOL/MicroJava/DFA/SemilatAlg.thy
changeset 61361 8b5f00202e1a
parent 58886 8a6cac7c7247
child 61994 133a8a888ae8
equal deleted inserted replaced
61360:a273bdac0934 61361:8b5f00202e1a
     1 (*  Title:      HOL/MicroJava/DFA/SemilatAlg.thy
     1 (*  Title:      HOL/MicroJava/DFA/SemilatAlg.thy
     2     Author:     Gerwin Klein
     2     Author:     Gerwin Klein
     3     Copyright   2002 Technische Universitaet Muenchen
     3     Copyright   2002 Technische Universitaet Muenchen
     4 *)
     4 *)
     5 
     5 
     6 section {* More on Semilattices *}
     6 section \<open>More on Semilattices\<close>
     7 
     7 
     8 theory SemilatAlg
     8 theory SemilatAlg
     9 imports Typing_Framework Product
     9 imports Typing_Framework Product
    10 begin
    10 begin
    11 
    11