# HG changeset patch
# User urbanc
# Date 1180066009 -7200
# Node ID 3d35c78b446fb977c9682611965bc9aa4979511e
# Parent  11e1a67fbfe8b71347d89876f25dc75b478ebedf
adapted to fix for fresh_fun_simp

diff -r 11e1a67fbfe8 -r 3d35c78b446f src/HOL/Nominal/Examples/Class.thy
--- 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