diff -r 4cc4390d5d25 -r 0321e89e66a3 Quotient-Paper/Paper.thy --- a/Quotient-Paper/Paper.thy Mon Jul 19 08:34:38 2010 +0100 +++ b/Quotient-Paper/Paper.thy Mon Jul 19 14:20:23 2010 +0100 @@ -15,6 +15,10 @@ compositions - explain how Quotient R Abs Rep is proved (j-version) - give an example where precise specification helps (core Haskell in nominal?) + + - Quote from Peter: + + One might think quotient have been studied to death, but *) notation (latex output)