author | bulwahn |
Thu, 17 Nov 2011 18:44:56 +0100 | |
changeset 45535 | fbad87611fae |
parent 45534 | 4ab21521b393 |
child 45536 | 5b0b1dc2e40f |
--- 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*}