# HG changeset patch
# User berghofe
# Date 1051049440 -7200
# Node ID 28ccb51bd2f303208a5254f7b0814f60523369f0
# Parent  026866537faeb953d6ff5ec05a4e64207ea3f299
Eliminated most occurrences of rule_format attribute.

diff -r 026866537fae -r 28ccb51bd2f3 src/HOL/Lambda/Lambda.thy
--- a/src/HOL/Lambda/Lambda.thy	Wed Apr 16 22:21:32 2003 +0200
+++ b/src/HOL/Lambda/Lambda.thy	Wed Apr 23 00:10:40 2003 +0200
@@ -182,21 +182,19 @@
 text {* Not used in Church-Rosser proof, but in Strong
   Normalization. \medskip *}
 
-theorem subst_preserves_beta [rule_format, simp]:
-    "r -> s ==> \<forall>t i. r[t/i] -> s[t/i]"
-  apply (erule beta.induct)
+theorem subst_preserves_beta [simp]:
+    "r -> s ==> (\<And>t i. r[t/i] -> s[t/i])"
+  apply (induct set: beta)
      apply (simp_all add: subst_subst [symmetric])
   done
 
-theorem lift_preserves_beta [rule_format, simp]:
-    "r -> s ==> \<forall>i. lift r i -> lift s i"
-  apply (erule beta.induct)
-     apply auto
-  done
+theorem lift_preserves_beta [simp]:
+    "r -> s ==> (\<And>i. lift r i -> lift s i)"
+  by (induct set: beta) auto
 
-theorem subst_preserves_beta2 [rule_format, simp]:
-    "\<forall>r s i. r -> s --> t[r/i] ->> t[s/i]"
-  apply (induct_tac t)
+theorem subst_preserves_beta2 [simp]:
+    "\<And>r s i. r -> s ==> t[r/i] ->> t[s/i]"
+  apply (induct t)
     apply (simp add: subst_Var r_into_rtrancl)
    apply (simp add: rtrancl_beta_App)
   apply (simp add: rtrancl_beta_Abs)
diff -r 026866537fae -r 28ccb51bd2f3 src/HOL/Lambda/ListApplication.thy
--- a/src/HOL/Lambda/ListApplication.thy	Wed Apr 16 22:21:32 2003 +0200
+++ b/src/HOL/Lambda/ListApplication.thy	Wed Apr 23 00:10:40 2003 +0200
@@ -18,18 +18,17 @@
    apply auto
   done
 
-lemma Var_eq_apps_conv [rule_format, iff]:
-    "\<forall>s. (Var m = s \<degree>\<degree> ss) = (Var m = s \<and> ss = [])"
-  apply (induct_tac ss)
+lemma Var_eq_apps_conv [iff]:
+    "\<And>s. (Var m = s \<degree>\<degree> ss) = (Var m = s \<and> ss = [])"
+  apply (induct ss)
    apply auto
   done
 
-lemma Var_apps_eq_Var_apps_conv [rule_format, iff]:
-    "\<forall>ss. (Var m \<degree>\<degree> rs = Var n \<degree>\<degree> ss) = (m = n \<and> rs = ss)"
-  apply (induct_tac rs rule: rev_induct)
+lemma Var_apps_eq_Var_apps_conv [iff]:
+    "\<And>ss. (Var m \<degree>\<degree> rs = Var n \<degree>\<degree> ss) = (m = n \<and> rs = ss)"
+  apply (induct rs rule: rev_induct)
    apply simp
    apply blast
-  apply (rule allI)
   apply (induct_tac ss rule: rev_induct)
    apply auto
   done
@@ -54,11 +53,10 @@
   done
 
 lemma Abs_apps_eq_Abs_apps_conv [iff]:
-    "\<forall>ss. (Abs r \<degree>\<degree> rs = Abs s \<degree>\<degree> ss) = (r = s \<and> rs = ss)"
-  apply (induct_tac rs rule: rev_induct)
+    "\<And>ss. (Abs r \<degree>\<degree> rs = Abs s \<degree>\<degree> ss) = (r = s \<and> rs = ss)"
+  apply (induct rs rule: rev_induct)
    apply simp
    apply blast
-  apply (rule allI)
   apply (induct_tac ss rule: rev_induct)
    apply auto
   done
@@ -69,11 +67,10 @@
    apply auto
   done
 
-lemma Var_apps_neq_Abs_apps [rule_format, iff]:
-    "\<forall>ts. Var n \<degree>\<degree> ts ~= Abs r \<degree>\<degree> ss"
-  apply (induct_tac ss rule: rev_induct)
+lemma Var_apps_neq_Abs_apps [iff]:
+    "\<And>ts. Var n \<degree>\<degree> ts ~= Abs r \<degree>\<degree> ss"
+  apply (induct ss rule: rev_induct)
    apply simp
-  apply (rule allI)
   apply (induct_tac ts rule: rev_induct)
    apply auto
   done