author | Christian Urban <urbanc@in.tum.de> |
Mon, 21 Jun 2010 00:45:27 +0100 | |
changeset 2286 | e7bc2ae30faf |
parent 2285 | 965ee8f08d4c |
child 2287 | adb5b1349280 |
--- a/Quotient-Paper/Paper.thy Mon Jun 21 00:36:17 2010 +0100 +++ b/Quotient-Paper/Paper.thy Mon Jun 21 00:45:27 2010 +0100 @@ -5,6 +5,14 @@ "../Nominal/FSet" begin +(**** + +** things to do for the next version +* +* - what are quot_thms? +* - what do all preservation theorems look like +*) + notation (latex output) rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and