src/HOLCF/Tools/Domain/domain_axioms.ML
changeset 35495 dc59e781669f
parent 35494 45c9a8278faf
child 35497 979706bd5c16
equal deleted inserted replaced
35494:45c9a8278faf 35495:dc59e781669f
   207     in
   207     in
   208       val thy =
   208       val thy =
   209           if definitional then thy
   209           if definitional then thy
   210           else fold ax_lub_take dnames thy
   210           else fold ax_lub_take dnames thy
   211     end;
   211     end;
   212 
       
   213     val use_copy_def = length eqs>1 andalso not definitional;
       
   214   in
   212   in
   215     thy
   213     thy
   216     |> Sign.add_path comp_dnam
   214     |> Sign.add_path comp_dnam
   217 (*
   215 (*
   218     |> add_defs_infer [bisim_def]
   216     |> add_defs_infer [bisim_def]