# HG changeset patch
# User urbanc
# Date 1178207676 -7200
# Node ID 18f4014e1259e024c468d93de374667cb3812380
# Parent  72a7b6ad153b4e43ec7547f23468745a58e780cc
tuned some of the proofs and added the lemma fresh_bool

diff -r 72a7b6ad153b -r 18f4014e1259 src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Wed May 02 21:00:06 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Thu May 03 17:54:36 2007 +0200
@@ -323,43 +323,43 @@
 lemma fresh_none:
   fixes a :: "'x"
   shows "a\<sharp>None"
-  apply(simp add: fresh_def supp_none)
-  done
+  by (simp add: fresh_def supp_none)
 
 lemma fresh_some:
   fixes a :: "'x"
   and   x :: "'a"
   shows "a\<sharp>(Some x) = a\<sharp>x"
-  apply(simp add: fresh_def supp_some)
-  done
+  by (simp add: fresh_def supp_some)
 
 lemma fresh_int:
   fixes a :: "'x"
   and   i :: "int"
   shows "a\<sharp>i"
-  apply(simp add: fresh_def supp_int)
-  done
+  by (simp add: fresh_def supp_int)
 
 lemma fresh_nat:
   fixes a :: "'x"
   and   n :: "nat"
   shows "a\<sharp>n"
-  apply(simp add: fresh_def supp_nat)
-  done
+  by (simp add: fresh_def supp_nat)
 
 lemma fresh_char:
   fixes a :: "'x"
   and   c :: "char"
   shows "a\<sharp>c"
-  apply(simp add: fresh_def supp_char)
-  done
+  by (simp add: fresh_def supp_char)
 
 lemma fresh_string:
   fixes a :: "'x"
   and   s :: "string"
   shows "a\<sharp>s"
-  apply(simp add: fresh_def supp_string)
-  done
+  by (simp add: fresh_def supp_string)
+
+lemma fresh_bool:
+  fixes a :: "'x"
+  and   b :: "bool"
+  shows "a\<sharp>b"
+  by (simp add: fresh_def supp_bool)
 
 text {* Normalization of freshness results; cf.\ @{text nominal_induct} *}