equal
deleted
inserted
replaced
121 |
121 |
122 (* ------------------------------------------------------------------------ *) |
122 (* ------------------------------------------------------------------------ *) |
123 (* type tr is flat *) |
123 (* type tr is flat *) |
124 (* ------------------------------------------------------------------------ *) |
124 (* ------------------------------------------------------------------------ *) |
125 |
125 |
126 qed_goalw "flat_tr" Tr1.thy [flat_def] "flat(TT)" |
126 qed_goalw "flat_tr" Tr1.thy [is_flat_def] "is_flat(TT)" |
127 (fn prems => |
127 (fn prems => |
128 [ |
128 [ |
129 (rtac allI 1), |
129 (rtac allI 1), |
130 (rtac allI 1), |
130 (rtac allI 1), |
131 (res_inst_tac [("p","x")] trE 1), |
131 (res_inst_tac [("p","x")] trE 1), |