# HG changeset patch
# User haftmann
# Date 1244445767 -7200
# Node ID bee3b47e15165a26ef5aaf56d9bfadcbe98ed1d6
# Parent  259a3c90016eeed241ddbf0972a57bb9799bc8ca
constant "chars" of all characters

diff -r 259a3c90016e -r bee3b47e1516 src/HOL/Library/Fin_Fun.thy
--- a/src/HOL/Library/Fin_Fun.thy	Mon Jun 08 08:38:53 2009 +0200
+++ b/src/HOL/Library/Fin_Fun.thy	Mon Jun 08 09:22:47 2009 +0200
@@ -1186,10 +1186,10 @@
 proof -
   from enum_distinct
   have "card (set (enum :: char list)) = length (enum :: char list)"
-    by -(rule distinct_card)
+    by - (rule distinct_card)
   also have "set enum = (UNIV :: char set)" by auto
-  also note enum_char
-  finally show ?thesis by simp
+  also note enum_chars
+  finally show ?thesis by (simp add: chars_def)
 qed
 
 instantiation char :: card_UNIV begin