# HG changeset patch
# User nipkow
# Date 855770079 -3600
# Node ID 4370e5f0fa3f79a7d044b3c1a8ea193740ff96f2
# Parent  450c9b682a924eca41a6e4dfacab6e2bf90f8669
New class "order" and accompanying changes.

diff -r 450c9b682a92 -r 4370e5f0fa3f src/HOL/Lex/AutoChopper.ML
--- a/src/HOL/Lex/AutoChopper.ML	Wed Feb 12 18:53:59 1997 +0100
+++ b/src/HOL/Lex/AutoChopper.ML	Wed Feb 12 18:54:39 1997 +0100
@@ -51,7 +51,7 @@
 goal AutoChopper.thy
 "! r erk l rst st ys yss zs::'a list. \
 \    acc xs st erk r (l,rst) A = (ys#yss, zs) --> \
-\    ys@flat(yss)@zs = (if acc_prefix A st xs then r@xs else erk@flat(l)@rst)";
+\    ys@concat(yss)@zs = (if acc_prefix A st xs then r@xs else erk@concat(l)@rst)";
 by (list.induct_tac "xs" 1);
  by (simp_tac (!simpset addcongs [conj_cong] setloop (split_tac [expand_if])) 1);
 by (asm_simp_tac (!simpset setloop (split_tac [expand_if])) 1);
@@ -133,7 +133,7 @@
  "! st erk r l rest ys yss zs. \
 \   acc xs st erk r (l,rest) A = (ys#yss, zs) --> \
 \     (if acc_prefix A st xs       \
-\      then acc(flat(yss)@zs)(start A) [] [] ([],flat(yss)@zs) A = (yss,zs) \
+\      then acc(concat(yss)@zs)(start A) [] [] ([],concat(yss)@zs) A = (yss,zs) \
 \      else (erk~=[] & (l,rest)=(yss,zs)) | (erk=[] & (l, rest)=(ys#yss,zs)))";
 by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
 by (list.induct_tac "xs" 1);
@@ -151,7 +151,7 @@
  by (subgoal_tac "r@[a] ~= []" 2);
   by (Fast_tac 2);
  by (Simp_tac 2);
-by (subgoal_tac "flat(yss) @ zs = list" 1);
+by (subgoal_tac "concat(yss) @ zs = list" 1);
  by (hyp_subst_tac 1);
  by (atac 1);
 by (case_tac "yss = []" 1);
diff -r 450c9b682a92 -r 4370e5f0fa3f src/HOL/Lex/Chopper.thy
--- a/src/HOL/Lex/Chopper.thy	Wed Feb 12 18:53:59 1997 +0100
+++ b/src/HOL/Lex/Chopper.thy	Wed Feb 12 18:54:39 1997 +0100
@@ -25,8 +25,8 @@
        (!zs. chopper(xs) = ([],zs) -->
              zs=xs & (!ys. ys ~= [] & ys <= xs --> ~L(ys))) &
        (!ys yss zs. chopper(xs) = (ys#yss,zs) -->
-          ys ~= [] & L(ys) & xs=ys@flat(yss)@zs &
-          chopper(flat(yss)@zs) = (yss,zs) &
+          ys ~= [] & L(ys) & xs=ys@concat(yss)@zs &
+          chopper(concat(yss)@zs) = (yss,zs) &
           (!as. as <= xs & ys <= as & ys ~= as --> ~L(as)))"
 
 end
diff -r 450c9b682a92 -r 4370e5f0fa3f src/HOL/ex/Puzzle.ML
--- a/src/HOL/ex/Puzzle.ML	Wed Feb 12 18:53:59 1997 +0100
+++ b/src/HOL/ex/Puzzle.ML	Wed Feb 12 18:54:39 1997 +0100
@@ -23,7 +23,7 @@
 by (subgoal_tac "f(na) <= f(f(na))" 1);
 by (fast_tac (!claset addIs [Puzzle.f_ax]) 2);
 by (rtac lessD 1);
-by (best_tac (!claset delrules [le_refl] 
+by (fast_tac (!claset delrules [order_refl] 
                       addIs [Puzzle.f_ax, le_less_trans]) 1);
 val lemma = result() RS spec RS mp;