equal
deleted
inserted
replaced
163 *---------------------------------------------------------------------------*) |
163 *---------------------------------------------------------------------------*) |
164 |
164 |
165 (** pred_sexp lemmas **) |
165 (** pred_sexp lemmas **) |
166 |
166 |
167 Goalw [CONS_def,In1_def] |
167 Goalw [CONS_def,In1_def] |
168 "!!M. [| M: sexp; N: sexp |] ==> (M, CONS M N) : pred_sexp^+"; |
168 "[| M: sexp; N: sexp |] ==> (M, CONS M N) : pred_sexp^+"; |
169 by (Asm_simp_tac 1); |
169 by (Asm_simp_tac 1); |
170 qed "pred_sexp_CONS_I1"; |
170 qed "pred_sexp_CONS_I1"; |
171 |
171 |
172 Goalw [CONS_def,In1_def] |
172 Goalw [CONS_def,In1_def] |
173 "!!M. [| M: sexp; N: sexp |] ==> (N, CONS M N) : pred_sexp^+"; |
173 "[| M: sexp; N: sexp |] ==> (N, CONS M N) : pred_sexp^+"; |
174 by (Asm_simp_tac 1); |
174 by (Asm_simp_tac 1); |
175 qed "pred_sexp_CONS_I2"; |
175 qed "pred_sexp_CONS_I2"; |
176 |
176 |
177 val [prem] = goal SList.thy |
177 val [prem] = goal SList.thy |
178 "(CONS M1 M2, N) : pred_sexp^+ ==> \ |
178 "(CONS M1 M2, N) : pred_sexp^+ ==> \ |