| changeset 66453 | cc19f7ca2ed6 | 
| parent 63167 | 0909deb8059b | 
| child 69597 | ff784d5a5bfb | 
--- a/src/HOL/Quotient_Examples/Quotient_Message.thy Fri Aug 18 13:55:05 2017 +0200 +++ b/src/HOL/Quotient_Examples/Quotient_Message.thy Fri Aug 18 20:47:47 2017 +0200 @@ -5,7 +5,7 @@ *) theory Quotient_Message -imports Main "~~/src/HOL/Library/Quotient_Syntax" +imports Main "HOL-Library.Quotient_Syntax" begin subsection\<open>Defining the Free Algebra\<close>