src/HOLCF/Pcpo.thy
changeset 33523 96730ad673be
parent 31076 99fe356cbbc2
child 35492 5d200f2d7a4f
equal deleted inserted replaced
33522:737589bb9bb8 33523:96730ad673be
   194 end
   194 end
   195 
   195 
   196 text {* Simproc to rewrite @{term "\<bottom> = x"} to @{term "x = \<bottom>"}. *}
   196 text {* Simproc to rewrite @{term "\<bottom> = x"} to @{term "x = \<bottom>"}. *}
   197 
   197 
   198 setup {*
   198 setup {*
   199   ReorientProc.add
   199   Reorient_Proc.add
   200     (fn Const(@{const_name UU}, _) => true | _ => false)
   200     (fn Const(@{const_name UU}, _) => true | _ => false)
   201 *}
   201 *}
   202 
   202 
   203 simproc_setup reorient_bottom ("\<bottom> = x") = ReorientProc.proc
   203 simproc_setup reorient_bottom ("\<bottom> = x") = Reorient_Proc.proc
   204 
   204 
   205 context pcpo
   205 context pcpo
   206 begin
   206 begin
   207 
   207 
   208 text {* useful lemmas about @{term \<bottom>} *}
   208 text {* useful lemmas about @{term \<bottom>} *}