equal
deleted
inserted
replaced
29 |
29 |
30 val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma); |
30 val (_ $ (_ $ (_ $ (distinct_f $ _) $ _))) = hd (prems_of distinct_lemma); |
31 |
31 |
32 (* figure out internal names *) |
32 (* figure out internal names *) |
33 |
33 |
34 val image_name = Sign.intern_const (Theory.sign_of Set.thy) "op ``"; |
34 val image_name = Sign.intern_const (Theory.sign_of Set.thy) "image"; |
35 val UNIV_name = Sign.intern_const (Theory.sign_of Set.thy) "UNIV"; |
35 val UNIV_name = Sign.intern_const (Theory.sign_of Set.thy) "UNIV"; |
36 val inj_on_name = Sign.intern_const (Theory.sign_of Fun.thy) "inj_on"; |
36 val inj_on_name = Sign.intern_const (Theory.sign_of Fun.thy) "inj_on"; |
37 val inv_name = Sign.intern_const (Theory.sign_of Fun.thy) "inv"; |
37 val inv_name = Sign.intern_const (Theory.sign_of Fun.thy) "inv"; |
38 |
38 |
39 fun exh_thm_of (dt_info : datatype_info Symtab.table) tname = |
39 fun exh_thm_of (dt_info : datatype_info Symtab.table) tname = |