src/HOL/Library/ExecutableSet.thy
changeset 23394 474ff28210c0
parent 22921 475ff421a6a3
     1.1 --- a/src/HOL/Library/ExecutableSet.thy	Thu Jun 14 23:04:36 2007 +0200
     1.2 +++ b/src/HOL/Library/ExecutableSet.thy	Thu Jun 14 23:04:39 2007 +0200
     1.3 @@ -56,10 +56,9 @@
     1.4    insertl :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
     1.5    "insertl x xs = (if member xs x then xs else x#xs)"
     1.6  
     1.7 -lemma
     1.8 -  [code target: List]: "member [] y \<longleftrightarrow> False"
     1.9 +lemma [code target: List]: "member [] y \<longleftrightarrow> False"
    1.10    and [code target: List]: "member (x#xs) y \<longleftrightarrow> y = x \<or> member xs y"
    1.11 -unfolding member_def by (induct xs) simp_all
    1.12 +  unfolding member_def by (induct xs) simp_all
    1.13  
    1.14  fun
    1.15    drop_first :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    1.16 @@ -201,7 +200,7 @@
    1.17    fixes ys
    1.18    assumes distnct: "distinct ys"
    1.19    shows "set (subtract' ys xs) = set ys - set xs"
    1.20 -  and "distinct (subtract' ys xs)"
    1.21 +    and "distinct (subtract' ys xs)"
    1.22    unfolding subtract'_def flip_def subtract_def
    1.23    using distnct by (induct xs arbitrary: ys) auto
    1.24  
    1.25 @@ -211,7 +210,8 @@
    1.26  
    1.27  lemma iso_unions:
    1.28    "set (unions xss) = \<Union> set (map set xss)"
    1.29 -unfolding unions_def proof (induct xss)
    1.30 +  unfolding unions_def
    1.31 +proof (induct xss)
    1.32    case Nil show ?case by simp
    1.33  next
    1.34    case (Cons xs xss) thus ?case by (induct xs) (simp_all add: iso_insert)