equal
deleted
inserted
replaced
167 in |
167 in |
168 thm' |
168 thm' |
169 end |
169 end |
170 |
170 |
171 fun str_of_thm ctxt thm = |
171 fun str_of_thm ctxt thm = |
172 let |
172 str_of_cterm ctxt (#prop (crep_thm (no_vars ctxt thm)))*} |
173 val {prop, ...} = crep_thm (no_vars ctxt thm) |
|
174 in |
|
175 str_of_cterm ctxt prop |
|
176 end*} |
|
177 |
173 |
178 text {* |
174 text {* |
179 Again the function @{ML commas} helps with printing more than one theorem. |
175 Again the function @{ML commas} helps with printing more than one theorem. |
180 *} |
176 *} |
181 |
177 |
531 |
527 |
532 *} |
528 *} |
533 |
529 |
534 ML{*fun make_imp P Q tau = |
530 ML{*fun make_imp P Q tau = |
535 let |
531 let |
536 val x = Free ("x",tau) |
532 val x = Free ("x", tau) |
537 in |
533 in |
538 Logic.all x (Logic.mk_implies (P $ x, Q $ x)) |
534 Logic.all x (Logic.mk_implies (P $ x, Q $ x)) |
539 end *} |
535 end *} |
540 |
536 |
541 text {* |
537 text {* |