changeset 45535 | fbad87611fae |
parent 41467 | 8fc17c5e11c0 |
child 47092 | fa3538d6004b |
--- a/src/HOL/Quotient_Examples/Quotient_Message.thy Thu Nov 17 14:35:32 2011 +0100 +++ b/src/HOL/Quotient_Examples/Quotient_Message.thy Thu Nov 17 18:44:56 2011 +0100 @@ -5,7 +5,7 @@ *) theory Quotient_Message -imports Main Quotient_Syntax +imports Main "~~/src/HOL/Library/Quotient_Syntax" begin subsection{*Defining the Free Algebra*}