equal
deleted
inserted
replaced
60 |
60 |
61 val field_radd = standard (radd_type RS field_rel_subset); |
61 val field_radd = standard (radd_type RS field_rel_subset); |
62 |
62 |
63 (** Linearity **) |
63 (** Linearity **) |
64 |
64 |
65 val sum_ss = ZF_ss addsimps [Pair_iff, InlI, InrI, Inl_iff, Inr_iff, |
|
66 Inl_Inr_iff, Inr_Inl_iff]; |
|
67 |
|
68 val radd_ss = sum_ss addsimps [radd_Inl_iff, radd_Inr_iff, |
65 val radd_ss = sum_ss addsimps [radd_Inl_iff, radd_Inr_iff, |
69 radd_Inl_Inr_iff, radd_Inr_Inl_iff]; |
66 radd_Inl_Inr_iff, radd_Inr_Inl_iff]; |
70 |
67 |
71 goalw OrderArith.thy [linear_def] |
68 goalw OrderArith.thy [linear_def] |
72 "!!r s. [| linear(A,r); linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))"; |
69 "!!r s. [| linear(A,r); linear(B,s) |] ==> linear(A+B,radd(A,r,B,s))"; |