--- 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