Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/HOL/Tools/Lifting/lifting_term.ML
changeset 54788 ee90c67502c9
parent 54356 ca237b9e4542
child 55223 03b10317ba78
equal deleted inserted replaced
54787:71a0a8687d6c 54788:ee90c67502c9 
   521       end
 
   521       end
 
   522     in
 
   522     in
 
   523       Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.fun2_conv parametrize_relation_conv)) thm
 
   523       Conv.fconv_rule (HOLogic.Trueprop_conv (Conv.fun2_conv parametrize_relation_conv)) thm
 
   524     end
 
   524     end
 
   525 
   525 
   526 end;
 
   526 end
wneuper/isa