9 

     9 

    10 quotient my_int = "nat \<times> nat" / intrel

    10 quotient my_int = "nat \<times> nat" / intrel

    11   apply(unfold EQUIV_def)

    11   apply(unfold EQUIV_def)

    12   apply(auto simp add: mem_def expand_fun_eq)

    12   apply(auto simp add: mem_def expand_fun_eq)

    13   done

    13   done

    14 

    16 

    15 typ my_int

    17 typ my_int

    16 

    18 

    17 local_setup {*

    19 local_setup {*

    18   make_const_def @{binding "ZERO"} @{term "(0::nat, 0::nat)"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd

    20   make_const_def @{binding "ZERO"} @{term "(0::nat, 0::nat)"} NoSyn @{typ "nat \<times> nat"} @{typ "my_int"} #> snd