src/HOL/Lambda/ListOrder.thy
changeset 9941 fe05af7ec816
parent 9906 5c027cca6262
child 10264 ef384b242d09
     1.1 --- a/src/HOL/Lambda/ListOrder.thy	Tue Sep 12 19:03:13 2000 +0200
     1.2 +++ b/src/HOL/Lambda/ListOrder.thy	Tue Sep 12 22:13:23 2000 +0200
     1.3 @@ -64,7 +64,7 @@
     1.4    apply (blast intro: append_eq_appendI)
     1.5    done
     1.6  
     1.7 -lemma Cons_step1E [rulified, elim!]:
     1.8 +lemma Cons_step1E [rule_format, elim!]:
     1.9    "[| (ys, x # xs) \<in> step1 r;
    1.10      \<forall>y. ys = y # xs --> (y, x) \<in> r --> R;
    1.11      \<forall>zs. ys = x # zs --> (zs, xs) \<in> step1 r --> R
    1.12 @@ -87,7 +87,7 @@
    1.13    apply blast
    1.14    done
    1.15  
    1.16 -lemma Cons_acc_step1I [rulified, intro!]:
    1.17 +lemma Cons_acc_step1I [rule_format, intro!]:
    1.18      "x \<in> acc r ==> \<forall>xs. xs \<in> acc (step1 r) --> x # xs \<in> acc (step1 r)"
    1.19    apply (erule acc_induct)
    1.20    apply (erule thin_rl)