Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/HOL/BNF/Tools/bnf_def.ML
changeset 55997 36301c99ed26
parent 55993 56fdc6412abc
child 56082 91f54d386680
equal deleted inserted replaced
55996:59388c359dec 55997:36301c99ed26 
   123 
   123 
   124 open BNF_Util
 
   124 open BNF_Util
 
   125 open BNF_Tactics
 
   125 open BNF_Tactics
 
   126 open BNF_Def_Tactics
 
   126 open BNF_Def_Tactics
 
   127 
   127 
   128 val cong_fundefcong_attrs = @{attributes [cong, fundef_cong]};
 
   128 val fundefcong_attrs = @{attributes [fundef_cong]};
 
   129 
   129 
   130 type axioms = {
 
   130 type axioms = {
 
   131   map_id0: thm,
 
   131   map_id0: thm,
 
   132   map_comp0: thm,
 
   132   map_comp0: thm,
 
   133   map_cong0: thm,
 
   133   map_cong0: thm,
 
   634     #> (if fact_policy <> Dont_Note then
 
   634     #> (if fact_policy <> Dont_Note then
 
   635         let
 
   635         let
 
   636           val notes =
 
   636           val notes =
 
   637             [(map_compN, [Lazy.force (#map_comp facts)], []),
 
   637             [(map_compN, [Lazy.force (#map_comp facts)], []),
 
   638             (map_cong0N, [#map_cong0 axioms], []),
 
   638             (map_cong0N, [#map_cong0 axioms], []),
 
   639             (map_congN, [Lazy.force (#map_cong facts)], cong_fundefcong_attrs),
 
   639             (map_congN, [Lazy.force (#map_cong facts)], fundefcong_attrs),
 
   640             (map_idN, [Lazy.force (#map_id facts)], []),
 
   640             (map_idN, [Lazy.force (#map_id facts)], []),
 
   641             (rel_comppN, [Lazy.force (#rel_OO facts)], []),
 
   641             (rel_comppN, [Lazy.force (#rel_OO facts)], []),
 
   642             (rel_compp_GrpN, no_refl [#rel_OO_Grp axioms], []),
 
   642             (rel_compp_GrpN, no_refl [#rel_OO_Grp axioms], []),
 
   643             (rel_conversepN, [Lazy.force (#rel_conversep facts)], []),
 
   643             (rel_conversepN, [Lazy.force (#rel_conversep facts)], []),
 
   644             (rel_eqN, [Lazy.force (#rel_eq facts)], []),
 
   644             (rel_eqN, [Lazy.force (#rel_eq facts)], []),
wneuper/isa