# HG changeset patch # User Cezary Kaliszyk # Date 1259932280 -3600 # Node ID 7ba2fc25c6a3af6ac8fffe833e4a52fa0b76c8d0 # Parent 3f657c4fbefa27e63c2574af502c4b83f0fd22a6# Parent c7c6ba5ac043c8ce32818dbae5d2819a91df8278 merge diff -r 3f657c4fbefa -r 7ba2fc25c6a3 FSet.thy --- a/FSet.thy Fri Dec 04 14:11:03 2009 +0100 +++ b/FSet.thy Fri Dec 04 14:11:20 2009 +0100 @@ -337,8 +337,6 @@ apply (tactic {* lift_tac_fset @{context} @{thm append_assoc} 1 *}) done -lemma cheat: "P" sorry - lemma "\P EMPTY; \a x. P x \ P (INSERT a x)\ \ P l" apply (tactic {* (ObjectLogic.full_atomize_tac THEN' gen_frees_tac @{context}) 1 *}) diff -r 3f657c4fbefa -r 7ba2fc25c6a3 QuotMain.thy --- a/QuotMain.thy Fri Dec 04 14:11:03 2009 +0100 +++ b/QuotMain.thy Fri Dec 04 14:11:20 2009 +0100 @@ -146,7 +146,7 @@ declare [[map "fun" = (fun_map, FUN_REL)]] lemmas [quotient_thm] = - FUN_QUOTIENT IDENTITY_QUOTIENT LIST_QUOTIENT + FUN_QUOTIENT LIST_QUOTIENT ML {* maps_lookup @{theory} "List.list" *} ML {* maps_lookup @{theory} "*" *}