equal
deleted
inserted
replaced
109 apply(cases b) |
109 apply(cases b) |
110 apply(auto) |
110 apply(auto) |
111 done |
111 done |
112 |
112 |
113 lemma ho_plus_rsp: |
113 lemma ho_plus_rsp: |
114 "IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel my_plus my_plus" |
114 "(intrel ===> intrel ===> intrel) my_plus my_plus" |
115 by (simp) |
115 by (simp) |
116 |
116 |
117 ML {* val consts = [@{const_name "my_plus"}] *} |
117 ML {* val consts = [@{const_name "my_plus"}] *} |
118 ML {* val rty = @{typ "nat \<times> nat"} *} |
118 ML {* val rty = @{typ "nat \<times> nat"} *} |
119 ML {* val qty = @{typ "my_int"} *} |
119 ML {* val qty = @{typ "my_int"} *} |