# HG changeset patch # User Cezary Kaliszyk # Date 1260606426 -3600 # Node ID 8d5408322de50529b6f0a52ed7e981d6bc0d01f5 # Parent 0015159fee9616cc7cacfc52eccb4968f6fa7b38 Minor diff -r 0015159fee96 -r 8d5408322de5 Quot/Examples/FSet3.thy --- a/Quot/Examples/FSet3.thy Sat Dec 12 05:12:50 2009 +0100 +++ b/Quot/Examples/FSet3.thy Sat Dec 12 09:27:06 2009 +0100 @@ -34,11 +34,11 @@ lemma no_mem_nil: - "(\a. \(a \ set A)) = (A = [])" + "(\a. a \ set A) = (A = [])" by (induct A) (auto) lemma none_mem_nil: - "(\a. \(a \ set A)) = (A \ [])" + "(\a. a \ set A) = (A \ [])" by simp lemma mem_cons: @@ -235,7 +235,7 @@ as "delete_raw" quotient_def - "funion :: 'a fset \ 'a fset \ 'a fset" ("_ \f _" [50, 51] 50) + "funion :: 'a fset \ 'a fset \ 'a fset" ("_ \f _" [50, 51] 50) as "op @" quotient_def @@ -267,6 +267,8 @@ MEM x [] = F MEM x (h::t) = (x=h) \/ MEM x t *) thm none_mem_nil +(*lemma "(\a. a \f A) = (A = fempty)"*) + thm mem_cons thm finite_set_raw_strong_cases thm card_raw.simps