Quotient-Paper/Paper.thy
changeset 2192 87024a9a9d89
parent 2191 8fdfbec54229
child 2193 aae246e2a5dc
equal deleted inserted replaced
2191:8fdfbec54229 2192:87024a9a9d89
   296   present in composition quotients. An example composition quotient
   296   present in composition quotients. An example composition quotient
   297   theorem that needs to be proved is the one needed to lift theorems
   297   theorem that needs to be proved is the one needed to lift theorems
   298   about concat:
   298   about concat:
   299 
   299 
   300   @{thm [display] quotient_compose_list[no_vars]}
   300   @{thm [display] quotient_compose_list[no_vars]}
       
   301 *}
       
   302 
   301 
   303 
   302 section {* Lifting Theorems *}
   304 section {* Lifting Theorems *}
   303 
   305 
   304 text {* TBD *}
   306 text {* TBD *}
   305 
   307