Quotient-Paper/Paper.thy
changeset 2374 0321e89e66a3
parent 2373 4cc4390d5d25
child 2377 273f57049bd1
equal deleted inserted replaced
2373:4cc4390d5d25 2374:0321e89e66a3
    13 * - what do all preservation theorems look like,
    13 * - what do all preservation theorems look like,
    14     in particular preservation for quotient
    14     in particular preservation for quotient
    15     compositions
    15     compositions
    16   - explain how Quotient R Abs Rep is proved (j-version)
    16   - explain how Quotient R Abs Rep is proved (j-version)
    17   - give an example where precise specification helps (core Haskell in nominal?)
    17   - give an example where precise specification helps (core Haskell in nominal?)
       
    18 
       
    19   - Quote from Peter:
       
    20 
       
    21     One might think quotient have been studied to death, but
    18 *)
    22 *)
    19 
    23 
    20 notation (latex output)
    24 notation (latex output)
    21   rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and
    25   rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and
    22   pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and
    26   pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and