equal
deleted
inserted
replaced
66 |
66 |
67 (* ------------------------------------------------------------------------ *) |
67 (* ------------------------------------------------------------------------ *) |
68 (* one is flat *) |
68 (* one is flat *) |
69 (* ------------------------------------------------------------------------ *) |
69 (* ------------------------------------------------------------------------ *) |
70 |
70 |
71 qed_goalw "flat_one" One.thy [flat_def] "flat(one)" |
71 qed_goalw "flat_one" One.thy [is_flat_def] "is_flat(one)" |
72 (fn prems => |
72 (fn prems => |
73 [ |
73 [ |
74 (rtac allI 1), |
74 (rtac allI 1), |
75 (rtac allI 1), |
75 (rtac allI 1), |
76 (res_inst_tac [("p","x")] oneE 1), |
76 (res_inst_tac [("p","x")] oneE 1), |