src/HOLCF/Pcpo.thy
changeset 28262 aa7ca36d67fd
parent 27415 be852e06d546
child 29138 661a8db7e647
equal deleted inserted replaced
28261:045187fc7840 28262:aa7ca36d67fd
   207       | Const("HOL.one", _) => NONE
   207       | Const("HOL.one", _) => NONE
   208       | Const("Numeral.number_of", _) $ _ => NONE
   208       | Const("Numeral.number_of", _) $ _ => NONE
   209       | _ => SOME meta_UU_reorient;
   209       | _ => SOME meta_UU_reorient;
   210 in
   210 in
   211   val UU_reorient_simproc = 
   211   val UU_reorient_simproc = 
   212     Simplifier.simproc @{theory} "UU_reorient_simproc" ["UU=x"] reorient_proc
   212     Simplifier.simproc (the_context ()) "UU_reorient_simproc" ["UU=x"] reorient_proc
   213 end;
   213 end;
   214 
   214 
   215 Addsimprocs [UU_reorient_simproc];
   215 Addsimprocs [UU_reorient_simproc];
   216 *}
   216 *}
   217 
   217