# HG changeset patch
# User haftmann
# Date 1449126657 -3600
# Node ID 9f4f0dc7be2c409c5ec7262fde6287ad1d9a9234
# Parent  f9e05eab6e3c6d99e171c4f5abd396f54f003366
modernized

diff -r f9e05eab6e3c -r 9f4f0dc7be2c src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Thu Dec 03 08:10:56 2015 +0100
+++ b/src/HOL/Finite_Set.thy	Thu Dec 03 08:10:57 2015 +0100
@@ -1209,17 +1209,9 @@
   But now that we have @{const fold} things are easy:
 \<close>
 
-definition card :: "'a set \<Rightarrow> nat" where
-  "card = folding.F (\<lambda>_. Suc) 0"
-
-interpretation card: folding "\<lambda>_. Suc" 0
-rewrites
-  "folding.F (\<lambda>_. Suc) 0 = card"
-proof -
-  show "folding (\<lambda>_. Suc)" by standard rule
-  then interpret card: folding "\<lambda>_. Suc" 0 .
-  from card_def show "folding.F (\<lambda>_. Suc) 0 = card" by rule
-qed
+permanent_interpretation card: folding "\<lambda>_. Suc" 0
+  defines card = "folding.F (\<lambda>_. Suc) 0"
+  by standard rule
 
 lemma card_infinite:
   "\<not> finite A \<Longrightarrow> card A = 0"