src/HOL/Algebra/Lattice.thy
changeset 35849 b5522b51cb1e
parent 35848 5443079512ea
child 39990 9b4341366b63
     1.1 --- a/src/HOL/Algebra/Lattice.thy	Sun Mar 21 16:51:37 2010 +0100
     1.2 +++ b/src/HOL/Algebra/Lattice.thy	Sun Mar 21 17:12:31 2010 +0100
     1.3 @@ -1,12 +1,13 @@
     1.4 -(*
     1.5 -  Title:     HOL/Algebra/Lattice.thy
     1.6 -  Author:    Clemens Ballarin, started 7 November 2003
     1.7 -  Copyright: Clemens Ballarin
     1.8 +(*  Title:      HOL/Algebra/Lattice.thy
     1.9 +    Author:     Clemens Ballarin, started 7 November 2003
    1.10 +    Copyright:  Clemens Ballarin
    1.11  
    1.12  Most congruence rules by Stephan Hohe.
    1.13  *)
    1.14  
    1.15 -theory Lattice imports Congruence begin
    1.16 +theory Lattice
    1.17 +imports Congruence
    1.18 +begin
    1.19  
    1.20  section {* Orders and Lattices *}
    1.21