changeset 61566 | c3d6e570ccef |
parent 61518 | ff12606337e9 |
child 61605 | 1bf7b186542e |
--- a/src/HOL/Finite_Set.thy Wed Nov 04 08:13:49 2015 +0100 +++ b/src/HOL/Finite_Set.thy Wed Nov 04 08:13:52 2015 +0100 @@ -1197,7 +1197,7 @@ "card = folding.F (\<lambda>_. Suc) 0" interpretation card!: folding "\<lambda>_. Suc" 0 -where +rewrites "folding.F (\<lambda>_. Suc) 0 = card" proof - show "folding (\<lambda>_. Suc)" by standard rule