src/HOL/Quotient_Examples/Quotient_Message.thy
changeset 41467 8fc17c5e11c0
parent 40823 37b25a87d7ef
child 45535 fbad87611fae
     1.1 --- a/src/HOL/Quotient_Examples/Quotient_Message.thy	Fri Jan 07 23:46:06 2011 +0100
     1.2 +++ b/src/HOL/Quotient_Examples/Quotient_Message.thy	Sat Jan 08 00:02:11 2011 +0100
     1.3 @@ -3,6 +3,7 @@
     1.4  
     1.5  Message datatype, based on an older version by Larry Paulson.
     1.6  *)
     1.7 +
     1.8  theory Quotient_Message
     1.9  imports Main Quotient_Syntax
    1.10  begin