| changeset 273 | b82e765ca464 |
| parent 270 | c55883442514 |
| child 274 | df225aa45770 |
| 272:ddd2f209d0d2 | 273:b82e765ca464 |
|---|---|
1056 in |
1056 in |
1057 ObjectLogic.rulify t_r |
1057 ObjectLogic.rulify t_r |
1058 end |
1058 end |
1059 *} |
1059 *} |
1060 |
1060 |
1061 |
1061 ML {* |
1062 end |
1062 fun lift_thm_note qty qty_name rsp_thms defs thm name lthy = |
1063 |
1063 let |
1064 val lifted_thm = lift_thm lthy qty qty_name rsp_thms defs thm; |
|
1065 val (_, lthy2) = note (name, lifted_thm) lthy; |
|
1066 in |
|
1067 lthy2 |
|
1068 end; |
|
1069 *} |
|
1070 |
|
1071 |
|
1072 end |
|
1073 |