Mercurial Mercurial > hg > nominal2 / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Quot/quotient_tacs.ML
changeset 913 b1f55dd64481
parent 911 95ee248b3832
child 920 dae99175f584
equal deleted inserted replaced
912:aa960d16570f 913:b1f55dd64481 
   429 fun fun_map_simple_conv xs ctrm =
 
   429 fun fun_map_simple_conv xs ctrm =
 
   430   case (term_of ctrm) of
 
   430   case (term_of ctrm) of
 
   431     ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
 
   431     ((Const (@{const_name "fun_map"}, _) $ _ $ _) $ h $ _) =>
 
   432         if (member (op=) xs h)
 
   432         if (member (op=) xs h)
 
   433         then Conv.all_conv ctrm
 
   433         then Conv.all_conv ctrm
 
   434         else Conv.rewr_conv @{thm fun_map.simps[THEN eq_reflection]} ctrm 
   434         else Conv.rewr_conv @{thm fun_map_def[THEN eq_reflection]} ctrm 
   435   | _ => Conv.all_conv ctrm
 
   435   | _ => Conv.all_conv ctrm
 
   436 
   436 
   437 fun fun_map_conv xs ctxt ctrm =
 
   437 fun fun_map_conv xs ctxt ctrm =
 
   438   case (term_of ctrm) of
 
   438   case (term_of ctrm) of
 
   439       _ $ _ => (Conv.comb_conv (fun_map_conv xs ctxt) then_conv
 
   439       _ $ _ => (Conv.comb_conv (fun_map_conv xs ctxt) then_conv
nominal2