--- a/src/HOL/Lex/AutoChopper.ML Wed Oct 25 18:36:01 2000 +0200
+++ b/src/HOL/Lex/AutoChopper.ML Wed Oct 25 18:39:01 2000 +0200
@@ -18,7 +18,7 @@
Goalw [acc_prefix_def]
"acc_prefix A (x#xs) s = (fin A (next A x s) | acc_prefix A xs (next A x s))";
-by (simp_tac (simpset() addsimps [prefix_Cons]) 1);
+by (simp_tac (simpset() addsimps [thm "prefix_Cons"]) 1);
by Safe_tac;
by (Asm_full_simp_tac 1);
by (case_tac "zs=[]" 1);
@@ -48,7 +48,7 @@
by (strip_tac 1);
by (rtac conjI 1);
by (Fast_tac 1);
-by (simp_tac (simpset() addsimps [prefix_Cons] addcongs [conj_cong]) 1);
+by (simp_tac (simpset() addsimps [thm "prefix_Cons"] addcongs [conj_cong]) 1);
by (strip_tac 1);
by (REPEAT(eresolve_tac [conjE,exE] 1));
by (hyp_subst_tac 1);
--- a/src/HOL/Lex/AutoChopper.thy Wed Oct 25 18:36:01 2000 +0200
+++ b/src/HOL/Lex/AutoChopper.thy Wed Oct 25 18:39:01 2000 +0200
@@ -19,7 +19,7 @@
its antecedents.
*)
-AutoChopper = Prefix + DA + Chopper +
+AutoChopper = DA + Chopper +
constdefs
is_auto_chopper :: (('a,'s)da => 'a chopper) => bool
--- a/src/HOL/Lex/Chopper.thy Wed Oct 25 18:36:01 2000 +0200
+++ b/src/HOL/Lex/Chopper.thy Wed Oct 25 18:39:01 2000 +0200
@@ -15,7 +15,7 @@
i.e. a set of strings.
*)
-Chopper = Prefix +
+Chopper = List_Prefix +
types 'a chopper = "'a list => 'a list list * 'a list"
--- a/src/HOL/Lex/MaxChop.ML Wed Oct 25 18:36:01 2000 +0200
+++ b/src/HOL/Lex/MaxChop.ML Wed Oct 25 18:39:01 2000 +0200
@@ -83,16 +83,16 @@
by (split_asm_tac [list.split_asm] 1);
by (Asm_full_simp_tac 1);
by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
- by (blast_tac (claset() addIs [prefix_append RS iffD2]) 1);
+ by (blast_tac (claset() addIs [thm "prefix_append" RS iffD2]) 1);
by (rtac conjI 1);
by (Clarify_tac 1);
by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
- by (blast_tac (claset() addIs [prefix_append RS iffD2]) 1);
+ by (blast_tac (claset() addIs [thm "prefix_append" RS iffD2]) 1);
by (Clarify_tac 1);
by (rename_tac "us uss" 1);
by (subgoal_tac "xs1=us" 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
-by (blast_tac (claset() addIs [prefix_append RS iffD2,prefix_antisym]) 1);
+by (blast_tac (claset() addIs [thm "prefix_append" RS iffD2, order_antisym]) 1);
qed "is_maxchopper_chop";
--- a/src/HOL/Lex/MaxPrefix.ML Wed Oct 25 18:36:01 2000 +0200
+++ b/src/HOL/Lex/MaxPrefix.ML Wed Oct 25 18:39:01 2000 +0200
@@ -19,7 +19,7 @@
by (Asm_simp_tac 1);
by (subgoal_tac "? us. us <= a # list & P (ps @ us)" 1);
by (Asm_simp_tac 1);
- by (blast_tac (claset() addIs [prefix_Cons RS iffD2]) 1);
+ by (blast_tac (claset() addIs [thm "prefix_Cons" RS iffD2]) 1);
by (subgoal_tac "~P(ps@[a])" 1);
by (Blast_tac 2);
by (Asm_simp_tac 1);
@@ -28,12 +28,12 @@
by (Clarify_tac 1);
by (case_tac "us" 1);
by (rtac iffI 1);
- by (asm_full_simp_tac (simpset() addsimps [prefix_Cons,prefix_append]) 1);
+ by (asm_full_simp_tac (simpset() addsimps [thm "prefix_Cons", thm "prefix_append"]) 1);
by (Blast_tac 1);
- by (asm_full_simp_tac (simpset() addsimps [prefix_Cons,prefix_append]) 1);
+ by (asm_full_simp_tac (simpset() addsimps [thm "prefix_Cons", thm "prefix_append"]) 1);
by (Clarify_tac 1);
by (etac disjE 1);
- by (fast_tac (claset() addDs [prefix_antisym]) 1);
+ by (fast_tac (claset() addDs [order_antisym]) 1);
by (Clarify_tac 1);
by (etac disjE 1);
by (Clarify_tac 1);
--- a/src/HOL/Lex/MaxPrefix.thy Wed Oct 25 18:36:01 2000 +0200
+++ b/src/HOL/Lex/MaxPrefix.thy Wed Oct 25 18:39:01 2000 +0200
@@ -4,7 +4,7 @@
Copyright 1998 TUM
*)
-MaxPrefix = Prefix +
+MaxPrefix = List_Prefix +
constdefs
is_maxpref :: ('a list => bool) => 'a list => 'a list => bool