equal
deleted
inserted
replaced
1315 ML_prf {* Thm.match (ct, goal') *} |
1315 ML_prf {* Thm.match (ct, goal') *} |
1316 ML_prf {* PRIMSEQ *} |
1316 ML_prf {* PRIMSEQ *} |
1317 ML_prf {* man_inst_norm *} |
1317 ML_prf {* man_inst_norm *} |
1318 apply (tactic {* compose_tac (false, man_inst_norm, 4) 1 *}) |
1318 apply (tactic {* compose_tac (false, man_inst_norm, 4) 1 *}) |
1319 |
1319 |
1320 |
1320 (* MINE *) |
1321 |
1321 apply (rule QUOTIENT_fset) |
1322 |
1322 |
|
1323 prefer 3 |
|
1324 (* ABS_REP_RSP *) |
|
1325 thm REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"] |
|
1326 apply (rule REP_ABS_RSP(1)[of "op \<approx>" "ABS_fset" "REP_fset"]) |
|
1327 (* MINE *) |
|
1328 apply (rule QUOTIENT_fset) |
|
1329 (* MINE *) |
|
1330 apply (rule list_eq_refl ) |
|
1331 prefer 2 |
|
1332 (* ABS_REP_RSP *) |
|
1333 apply (rule REP_ABS_RSP(1)[of "op \<approx> ===> op =" "REP_fset ---> id" "ABS_fset ---> id"]) |
|
1334 prefer 2 |
|
1335 (* MINE *) |
|
1336 apply (simp only: FUN_REL.simps) |
|
1337 prefer 3 |
|
1338 (* APPLY_RSP *) |
|
1339 thm APPLY_RSP |
1323 sorry |
1340 sorry |
1324 |
1341 |
1325 thm list.recs(2) |
1342 thm list.recs(2) |
1326 |
1343 |
1327 |
1344 |