forgotten selector
authortraytel
Fri Jul 17 16:13:03 2015 +0200 (2015-07-17)
changeset 607424050b243fc60
parent 60741 6349a28af772
child 60755 cde2b5d084e6
forgotten selector
src/HOL/Tools/BNF/bnf_def.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Thu Jul 16 18:36:16 2015 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Fri Jul 17 16:13:03 2015 +0200
     1.3 @@ -82,6 +82,7 @@
     1.4    val rel_mono_strong0_of_bnf: bnf -> thm
     1.5    val rel_mono_strong_of_bnf: bnf -> thm
     1.6    val rel_refl_of_bnf: bnf -> thm
     1.7 +  val rel_map_of_bnf: bnf -> thm list
     1.8    val rel_transfer_of_bnf: bnf -> thm
     1.9    val rel_eq_of_bnf: bnf -> thm
    1.10    val rel_flip_of_bnf: bnf -> thm
    1.11 @@ -485,6 +486,7 @@
    1.12  val rel_mono_strong0_of_bnf = Lazy.force o #rel_mono_strong0 o #facts o rep_bnf;
    1.13  val rel_mono_strong_of_bnf = Lazy.force o #rel_mono_strong o #facts o rep_bnf;
    1.14  val rel_refl_of_bnf = Lazy.force o #rel_refl o #facts o rep_bnf;
    1.15 +val rel_map_of_bnf = Lazy.force o #rel_map o #facts o rep_bnf;
    1.16  val rel_transfer_of_bnf = Lazy.force o #rel_transfer o #facts o rep_bnf;
    1.17  val rel_Grp_of_bnf = Lazy.force o #rel_Grp o #facts o rep_bnf;
    1.18  val rel_conversep_of_bnf = Lazy.force o #rel_conversep o #facts o rep_bnf;