Quotient-Paper/Paper.thy
changeset 2414 67e57fc3cd2a
parent 2413 1341a2d7570f
child 2416 12283a96e851
equal deleted inserted replaced
2413:1341a2d7570f 2414:67e57fc3cd2a
    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 
    18 
    19   - Quote from Peter:
    19   - Quote from Peter:
    20 
    20 
    21     One might think quotient have been studied to death, but
    21     One might think quotient have been studied to death, but
       
    22 
       
    23   - Mention Andreas Lochbiler in Acknowledgements and 'desceding'.
       
    24 
    22 *)
    25 *)
    23 
    26 
    24 notation (latex output)
    27 notation (latex output)
    25   rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and
    28   rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and
    26   pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and
    29   pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and