changeset 2377 | 273f57049bd1 |
parent 2376 | 44a5388d1d30 |
parent 2374 | 0321e89e66a3 |
child 2412 | 63f0e7f914dd |
--- a/Quotient-Paper/Paper.thy Mon Jul 19 08:55:49 2010 +0100 +++ b/Quotient-Paper/Paper.thy Tue Jul 20 06:14:16 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)