diff -r f3615235dc4d -r e3735771e7ba src/HOL/Nominal/Examples/Class.thy
--- a/src/HOL/Nominal/Examples/Class.thy	Thu May 24 12:09:38 2007 +0200
+++ b/src/HOL/Nominal/Examples/Class.thy	Thu May 24 13:59:54 2007 +0200
@@ -1,6 +1,6 @@
 (* $Id$ *)
 
-theory ClassWork 
+theory Class
 imports "Nominal" 
 begin
 
@@ -16810,7 +16810,6 @@
 apply(simp)
 apply(simp)
 apply(fresh_fun_simp)
-apply(fresh_fun_simp)
 apply(simp)
 (* other case of in BINDING *)
 apply(drule fin_elims)
@@ -16832,7 +16831,6 @@
 apply(simp)
 apply(simp)
 apply(fresh_fun_simp)
-apply(fresh_fun_simp)
 apply(simp)
 (* none of them in BINDING *)
 apply(simp)
@@ -16893,7 +16891,6 @@
 apply(simp add: abs_fresh fresh_prod fresh_atm)
 apply(simp)
 apply(fresh_fun_simp)
-apply(fresh_fun_simp)
 apply(simp)
 (* other case of in BINDING *)
 apply(drule fin_elims)
@@ -16915,7 +16912,6 @@
 apply(simp add: abs_fresh fresh_prod fresh_atm) 
 apply(simp add: abs_fresh fresh_prod fresh_atm)
 apply(fresh_fun_simp)
-apply(fresh_fun_simp)
 apply(simp)
 (* none of them in BINDING *)
 apply(simp)
@@ -16976,7 +16972,6 @@
 apply(simp add: abs_fresh fresh_prod fresh_atm)
 apply(simp)
 apply(fresh_fun_simp)
-apply(fresh_fun_simp)
 apply(simp)
 (* other case of in BINDING *)
 apply(drule fin_elims)
@@ -16998,7 +16993,6 @@
 apply(simp add: abs_fresh fresh_prod fresh_atm) 
 apply(simp add: abs_fresh fresh_prod fresh_atm)
 apply(fresh_fun_simp)
-apply(fresh_fun_simp)
 apply(simp)
 (* none of them in BINDING *)
 apply(simp)
@@ -17059,7 +17053,6 @@
 apply(simp add: abs_fresh fresh_prod fresh_atm)
 apply(simp add: abs_fresh)
 apply(fresh_fun_simp)
-apply(fresh_fun_simp)
 apply(simp)
 (* other case of in BINDING *)
 apply(drule fin_elims)
@@ -17081,7 +17074,6 @@
 apply(simp add: abs_fresh fresh_prod fresh_atm) 
 apply(simp add: abs_fresh fresh_prod fresh_atm)
 apply(fresh_fun_simp)
-apply(fresh_fun_simp)
 apply(simp)
 (* none of them in BINDING *)
 apply(simp)
@@ -17142,7 +17134,6 @@
 apply(simp add: abs_fresh fresh_prod fresh_atm)
 apply(simp add: abs_fresh)
 apply(fresh_fun_simp)
-apply(fresh_fun_simp)
 apply(simp)
 (* other case of in BINDING *)
 apply(drule fin_elims)
@@ -17164,7 +17155,6 @@
 apply(simp add: abs_fresh fresh_prod fresh_atm) 
 apply(simp add: abs_fresh fresh_prod fresh_atm)
 apply(fresh_fun_simp)
-apply(fresh_fun_simp)
 apply(simp)
 (* none of them in BINDING *)
 apply(simp)
@@ -17226,7 +17216,6 @@
 apply(simp add: abs_fresh)
 apply(simp)
 apply(fresh_fun_simp)
-apply(fresh_fun_simp)
 apply(simp)
 (* other case of in BINDING *)
 apply(drule fin_elims)
@@ -17251,11 +17240,9 @@
 apply(simp)
 apply(fresh_fun_simp)
 apply(simp add: abs_fresh abs_supp fin_supp)
-apply(fresh_fun_simp)
 apply(simp add: abs_fresh abs_supp fin_supp)
 apply(simp)
 (* none of them in BINDING *)
-apply(simp)
 apply(erule conjE)
 apply(frule CAND_ImpL_elim)
 apply(assumption)
@@ -17380,9 +17367,6 @@
 done
 
 
-(* HERE *)
-
-
 (* parallel substitution *)
 
 
@@ -18266,61 +18250,61 @@
 apply(simp)
 apply(auto)[1]
 apply(generate_fresh "coname")
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
 apply(simp)
 apply(case_tac "findn \<theta>n name")
 apply(simp)
 apply(auto)[1]
 apply(generate_fresh "name")
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
 apply(simp)
 apply(case_tac "findc \<theta>c coname3")
 apply(simp)
 apply(auto)[1]
 apply(generate_fresh "coname")
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
 apply(simp)
 apply(case_tac "findn \<theta>n name2")
 apply(simp)
 apply(auto)[1]
 apply(generate_fresh "name")
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
 apply(simp)
 apply(case_tac "findn \<theta>n name2")
 apply(simp)
 apply(auto)[1]
 apply(generate_fresh "name")
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
 apply(simp)
 apply(case_tac "findc \<theta>c coname2")
 apply(simp)
 apply(auto)[1]
 apply(generate_fresh "coname")
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
 apply(simp)
 apply(case_tac "findc \<theta>c coname2")
 apply(simp)
 apply(auto)[1]
 apply(generate_fresh "coname")
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
 apply(simp)
 apply(case_tac "findn \<theta>n name3")
 apply(simp)
 apply(auto)[1]
 apply(generate_fresh "name")
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
 apply(simp)
 apply(case_tac "findc \<theta>c coname2")
 apply(simp)
 apply(auto)[1]
 apply(generate_fresh "coname")
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
 apply(simp)
 apply(case_tac "findn \<theta>n name2")
 apply(simp)
 apply(auto)[1]
 apply(generate_fresh "name")
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
 apply(simp)
 done