src/HOL/Library/Nested_Environment.thy
changeset 23394 474ff28210c0
parent 20503 503ac4c5ef91
child 24433 4a405457e9d6
     1.1 --- a/src/HOL/Library/Nested_Environment.thy	Thu Jun 14 23:04:36 2007 +0200
     1.2 +++ b/src/HOL/Library/Nested_Environment.thy	Thu Jun 14 23:04:39 2007 +0200
     1.3 @@ -103,7 +103,7 @@
     1.4  theorem lookup_append_none:
     1.5    assumes "lookup env xs = None"
     1.6    shows "lookup env (xs @ ys) = None"
     1.7 -  using prems
     1.8 +  using assms
     1.9  proof (induct xs arbitrary: env)
    1.10    case Nil
    1.11    then have False by simp
    1.12 @@ -140,7 +140,7 @@
    1.13  theorem lookup_append_some:
    1.14    assumes "lookup env xs = Some e"
    1.15    shows "lookup env (xs @ ys) = lookup e ys"
    1.16 -  using prems
    1.17 +  using assms
    1.18  proof (induct xs arbitrary: env e)
    1.19    case Nil
    1.20    then have "env = e" by simp
    1.21 @@ -190,7 +190,7 @@
    1.22    assumes "lookup env (xs @ ys) = Some e"
    1.23    shows "\<exists>e. lookup env xs = Some e"
    1.24  proof -
    1.25 -  from prems have "lookup env (xs @ ys) \<noteq> None" by simp
    1.26 +  from assms have "lookup env (xs @ ys) \<noteq> None" by simp
    1.27    then have "lookup env xs \<noteq> None"
    1.28      by (rule contrapos_nn) (simp only: lookup_append_none)
    1.29    then show ?thesis by (simp)
    1.30 @@ -208,7 +208,7 @@
    1.31      lookup env xs = Some (Env b' es') \<and>
    1.32      es' y = Some env' \<and>
    1.33      lookup env' ys = Some e"
    1.34 -  using prems
    1.35 +  using assms
    1.36  proof (induct xs arbitrary: env e)
    1.37    case Nil
    1.38    from Nil.prems have "lookup env (y # ys) = Some e"
    1.39 @@ -328,7 +328,7 @@
    1.40  theorem lookup_update_some:
    1.41    assumes "lookup env xs = Some e"
    1.42    shows "lookup (update xs (Some env') env) xs = Some env'"
    1.43 -  using prems
    1.44 +  using assms
    1.45  proof (induct xs arbitrary: env e)
    1.46    case Nil
    1.47    then have "env = e" by simp
    1.48 @@ -377,7 +377,7 @@
    1.49  theorem update_append_none:
    1.50    assumes "lookup env xs = None"
    1.51    shows "update (xs @ y # ys) opt env = env"
    1.52 -  using prems
    1.53 +  using assms
    1.54  proof (induct xs arbitrary: env)
    1.55    case Nil
    1.56    then have False by simp
    1.57 @@ -420,7 +420,7 @@
    1.58  theorem update_append_some:
    1.59    assumes "lookup env xs = Some e"
    1.60    shows "lookup (update (xs @ y # ys) opt env) xs = Some (update (y # ys) opt e)"
    1.61 -  using prems
    1.62 +  using assms
    1.63  proof (induct xs arbitrary: env e)
    1.64    case Nil
    1.65    then have "env = e" by simp