equal
deleted
inserted
replaced
1235 (* MINE *) |
1235 (* MINE *) |
1236 apply (simp only: FUN_REL.simps) |
1236 apply (simp only: FUN_REL.simps) |
1237 prefer 3 |
1237 prefer 3 |
1238 (* APPLY_RSP *) |
1238 (* APPLY_RSP *) |
1239 thm APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"] |
1239 thm APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"] |
1240 apply (rule APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"]) |
1240 apply (rule_tac APPLY_RSP[of "op \<approx>" "ABS_fset" "REP_fset" "op =" "id" "id"]) |
|
1241 (* MINE *) |
|
1242 prefer 4 |
|
1243 apply (rule list_eq_refl ) |
|
1244 |
1241 sorry |
1245 sorry |
1242 |
1246 |
1243 thm list.recs(2) |
1247 thm list.recs(2) |
1244 |
1248 |
1245 |
1249 |