--- a/src/HOL/Nominal/Examples/Class.thy Fri May 25 05:18:56 2007 +0200
+++ b/src/HOL/Nominal/Examples/Class.thy Fri May 25 06:06:49 2007 +0200
@@ -16809,7 +16809,7 @@
apply(rule better_LNot_intro)
apply(simp)
apply(simp)
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
apply(simp)
(* other case of in BINDING *)
apply(drule fin_elims)
@@ -16830,7 +16830,7 @@
apply(rule better_LNot_intro)
apply(simp)
apply(simp)
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
apply(simp)
(* none of them in BINDING *)
apply(simp)
@@ -16890,7 +16890,7 @@
apply(rule better_LAnd1_intro)
apply(simp add: abs_fresh fresh_prod fresh_atm)
apply(simp)
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
apply(simp)
(* other case of in BINDING *)
apply(drule fin_elims)
@@ -16911,7 +16911,7 @@
apply(rule better_LAnd1_intro)
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 (no_asm))
apply(simp)
(* none of them in BINDING *)
apply(simp)
@@ -16971,7 +16971,7 @@
apply(rule better_LAnd2_intro)
apply(simp add: abs_fresh fresh_prod fresh_atm)
apply(simp)
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
apply(simp)
(* other case of in BINDING *)
apply(drule fin_elims)
@@ -16992,7 +16992,7 @@
apply(rule better_LAnd2_intro)
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 (no_asm))
apply(simp)
(* none of them in BINDING *)
apply(simp)
@@ -17052,7 +17052,7 @@
apply(rule better_LOr1_intro)
apply(simp add: abs_fresh fresh_prod fresh_atm)
apply(simp add: abs_fresh)
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
apply(simp)
(* other case of in BINDING *)
apply(drule fin_elims)
@@ -17073,7 +17073,7 @@
apply(rule better_LOr1_intro)
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 (no_asm))
apply(simp)
(* none of them in BINDING *)
apply(simp)
@@ -17133,7 +17133,7 @@
apply(rule better_LOr2_intro)
apply(simp add: abs_fresh fresh_prod fresh_atm)
apply(simp add: abs_fresh)
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
apply(simp)
(* other case of in BINDING *)
apply(drule fin_elims)
@@ -17154,7 +17154,7 @@
apply(rule better_LOr2_intro)
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 (no_asm))
apply(simp)
(* none of them in BINDING *)
apply(simp)
@@ -17215,7 +17215,7 @@
apply(simp add: abs_fresh fresh_prod fresh_atm)
apply(simp add: abs_fresh)
apply(simp)
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
apply(simp)
(* other case of in BINDING *)
apply(drule fin_elims)
@@ -17238,7 +17238,7 @@
apply(simp add: abs_fresh fresh_prod fresh_atm)
apply(simp add: abs_fresh fresh_prod fresh_atm)
apply(simp)
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
apply(simp add: abs_fresh abs_supp fin_supp)
apply(simp add: abs_fresh abs_supp fin_supp)
apply(simp)
@@ -18002,8 +18002,7 @@
apply(simp add: abs_fresh)
apply(auto)[1]
apply(generate_fresh "coname")
-apply(thin_tac "x1\<sharp>?p")
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
apply(drule cmaps_fresh)
apply(auto simp add: fresh_prod)[1]
apply(simp add: abs_fresh fresh_prod fresh_atm)
@@ -18011,8 +18010,7 @@
apply(simp add: abs_fresh)
apply(auto)[1]
apply(generate_fresh "name")
-apply(thin_tac "x1\<sharp>?p")
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
apply(drule nmaps_fresh)
apply(auto simp add: fresh_prod)[1]
apply(simp add: abs_fresh fresh_prod fresh_atm)
@@ -18020,9 +18018,7 @@
apply(simp add: abs_fresh)
apply(auto)[1]
apply(generate_fresh "coname")
-apply(thin_tac "x1\<sharp>?p")
-apply(thin_tac "x3\<sharp>?p")
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
apply(drule cmaps_fresh)
apply(auto simp add: fresh_prod)[1]
apply(simp add: abs_fresh fresh_prod fresh_atm)
@@ -18030,9 +18026,7 @@
apply(simp add: abs_fresh)
apply(auto)[1]
apply(generate_fresh "coname")
-apply(thin_tac "x1\<sharp>?p")
-apply(thin_tac "x3\<sharp>?p")
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
apply(drule_tac x="x3" in cmaps_fresh)
apply(auto simp add: fresh_prod)[1]
apply(simp add: abs_fresh fresh_prod fresh_atm)
@@ -18040,8 +18034,7 @@
apply(simp add: abs_fresh)
apply(auto)[1]
apply(generate_fresh "name")
-apply(thin_tac "x1\<sharp>?p")
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
apply(drule nmaps_fresh)
apply(auto simp add: fresh_prod)[1]
apply(simp add: abs_fresh fresh_prod fresh_atm)
@@ -18049,8 +18042,7 @@
apply(simp add: abs_fresh)
apply(auto)[1]
apply(generate_fresh "name")
-apply(thin_tac "x1\<sharp>?p")
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
apply(drule nmaps_fresh)
apply(auto simp add: fresh_prod)[1]
apply(simp add: abs_fresh fresh_prod fresh_atm)
@@ -18058,8 +18050,7 @@
apply(simp add: abs_fresh)
apply(auto)[1]
apply(generate_fresh "coname")
-apply(thin_tac "x1\<sharp>?p")
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
apply(drule cmaps_fresh)
apply(auto simp add: fresh_prod)[1]
apply(simp add: abs_fresh fresh_prod fresh_atm)
@@ -18067,8 +18058,7 @@
apply(simp add: abs_fresh)
apply(auto)[1]
apply(generate_fresh "coname")
-apply(thin_tac "x1\<sharp>?p")
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
apply(drule cmaps_fresh)
apply(auto simp add: fresh_prod)[1]
apply(simp add: abs_fresh fresh_prod fresh_atm)
@@ -18076,9 +18066,7 @@
apply(simp add: abs_fresh)
apply(auto)[1]
apply(generate_fresh "name")
-apply(thin_tac "x1\<sharp>?p")
-apply(thin_tac "x3\<sharp>?p")
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
apply(drule nmaps_fresh)
apply(auto simp add: fresh_prod)[1]
apply(simp add: abs_fresh fresh_prod fresh_atm)
@@ -18086,9 +18074,7 @@
apply(simp add: abs_fresh)
apply(auto)[1]
apply(generate_fresh "name")
-apply(thin_tac "x1\<sharp>?p")
-apply(thin_tac "x3\<sharp>?p")
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
apply(drule_tac a="x3" in nmaps_fresh)
apply(auto simp add: fresh_prod)[1]
apply(simp add: abs_fresh fresh_prod fresh_atm)
@@ -18096,9 +18082,7 @@
apply(simp add: abs_fresh abs_supp fin_supp)
apply(auto)[1]
apply(generate_fresh "coname")
-apply(thin_tac "x1\<sharp>?p")
-apply(thin_tac "x2\<sharp>?p")
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
apply(drule cmaps_fresh)
apply(auto simp add: fresh_prod)[1]
apply(simp add: abs_fresh fresh_prod fresh_atm abs_supp fin_supp)
@@ -18106,9 +18090,7 @@
apply(simp add: abs_fresh abs_supp fin_supp)
apply(auto)[1]
apply(generate_fresh "coname")
-apply(thin_tac "x1\<sharp>?p")
-apply(thin_tac "x2\<sharp>?p")
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
apply(drule_tac x="x2" in cmaps_fresh)
apply(auto simp add: fresh_prod)[1]
apply(simp add: abs_fresh fresh_prod fresh_atm abs_supp fin_supp)
@@ -18116,9 +18098,7 @@
apply(simp add: abs_fresh)
apply(auto)[1]
apply(generate_fresh "name")
-apply(thin_tac "x1\<sharp>?p")
-apply(thin_tac "x3\<sharp>?p")
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
apply(drule nmaps_fresh)
apply(auto simp add: fresh_prod)[1]
apply(simp add: abs_fresh fresh_prod fresh_atm)
@@ -18126,9 +18106,7 @@
apply(simp add: abs_fresh)
apply(auto)[1]
apply(generate_fresh "name")
-apply(thin_tac "x1\<sharp>?p")
-apply(thin_tac "x3\<sharp>?p")
-apply(fresh_fun_simp)
+apply(fresh_fun_simp (no_asm))
apply(drule_tac a="x3" in nmaps_fresh)
apply(auto simp add: fresh_prod)[1]
apply(simp add: abs_fresh fresh_prod fresh_atm)
@@ -18250,61 +18228,61 @@
apply(simp)
apply(auto)[1]
apply(generate_fresh "coname")
-apply(fresh_fun_simp (no_asm))
+apply(fresh_fun_simp)
apply(simp)
apply(case_tac "findn \<theta>n name")
apply(simp)
apply(auto)[1]
apply(generate_fresh "name")
-apply(fresh_fun_simp (no_asm))
+apply(fresh_fun_simp)
apply(simp)
apply(case_tac "findc \<theta>c coname3")
apply(simp)
apply(auto)[1]
apply(generate_fresh "coname")
-apply(fresh_fun_simp (no_asm))
+apply(fresh_fun_simp)
apply(simp)
apply(case_tac "findn \<theta>n name2")
apply(simp)
apply(auto)[1]
apply(generate_fresh "name")
-apply(fresh_fun_simp (no_asm))
+apply(fresh_fun_simp)
apply(simp)
apply(case_tac "findn \<theta>n name2")
apply(simp)
apply(auto)[1]
apply(generate_fresh "name")
-apply(fresh_fun_simp (no_asm))
+apply(fresh_fun_simp)
apply(simp)
apply(case_tac "findc \<theta>c coname2")
apply(simp)
apply(auto)[1]
apply(generate_fresh "coname")
-apply(fresh_fun_simp (no_asm))
+apply(fresh_fun_simp)
apply(simp)
apply(case_tac "findc \<theta>c coname2")
apply(simp)
apply(auto)[1]
apply(generate_fresh "coname")
-apply(fresh_fun_simp (no_asm))
+apply(fresh_fun_simp)
apply(simp)
apply(case_tac "findn \<theta>n name3")
apply(simp)
apply(auto)[1]
apply(generate_fresh "name")
-apply(fresh_fun_simp (no_asm))
+apply(fresh_fun_simp)
apply(simp)
apply(case_tac "findc \<theta>c coname2")
apply(simp)
apply(auto)[1]
apply(generate_fresh "coname")
-apply(fresh_fun_simp (no_asm))
+apply(fresh_fun_simp)
apply(simp)
apply(case_tac "findn \<theta>n name2")
apply(simp)
apply(auto)[1]
apply(generate_fresh "name")
-apply(fresh_fun_simp (no_asm))
+apply(fresh_fun_simp)
apply(simp)
done