equal
deleted
inserted
replaced
1192 thm m2_lift |
1192 thm m2_lift |
1193 (*thm card_suc*) |
1193 (*thm card_suc*) |
1194 |
1194 |
1195 thm leqi4_lift |
1195 thm leqi4_lift |
1196 ML {* |
1196 ML {* |
1197 val (nam, typ) = (hd (Term.add_vars (term_of (#prop (crep_thm @{thm leqi4_lift}))) [])) |
1197 val (nam, typ) = hd (Term.add_vars (prop_of @{thm leqi4_lift}) []) |
1198 val (_, l) = dest_Type typ |
1198 val (_, l) = dest_Type typ |
1199 val t = Type ("QuotMain.fset", l) |
1199 val t = Type ("QuotMain.fset", l) |
1200 val v = Var (nam, t) |
1200 val v = Var (nam, t) |
1201 val cv = cterm_of @{theory} ((term_of @{cpat "REP_fset"}) $ v) |
1201 val cv = cterm_of @{theory} ((term_of @{cpat "REP_fset"}) $ v) |
1202 *} |
1202 *} |
1210 *} |
1210 *} |
1211 |
1211 |
1212 (* |
1212 (* |
1213 thm card_suc |
1213 thm card_suc |
1214 ML {* |
1214 ML {* |
1215 val (nam, typ) = (hd (tl (Term.add_vars (term_of (#prop (crep_thm @{thm card_suc}))) []))) |
1215 val (nam, typ) = hd (tl (Term.add_vars (prop_of @{thm card_suc})) []) |
1216 val (_, l) = dest_Type typ |
1216 val (_, l) = dest_Type typ |
1217 val t = Type ("QuotMain.fset", l) |
1217 val t = Type ("QuotMain.fset", l) |
1218 val v = Var (nam, t) |
1218 val v = Var (nam, t) |
1219 val cv = cterm_of @{theory} ((term_of @{cpat "REP_fset"}) $ v) |
1219 val cv = cterm_of @{theory} ((term_of @{cpat "REP_fset"}) $ v) |
1220 *} |
1220 *} |