# HG changeset patch # User wenzelm # Date 972491941 -7200 # Node ID 291ce4c4b50e7d60094179e7758ee830971c1730 # Parent fca9cd9fd115efdc93e4dccdf52c5ca55881f4a8 use Library/List_Prefix; diff -r fca9cd9fd115 -r 291ce4c4b50e src/HOL/Lex/AutoChopper.ML --- 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); diff -r fca9cd9fd115 -r 291ce4c4b50e src/HOL/Lex/AutoChopper.thy --- 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 diff -r fca9cd9fd115 -r 291ce4c4b50e src/HOL/Lex/Chopper.thy --- 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" diff -r fca9cd9fd115 -r 291ce4c4b50e src/HOL/Lex/MaxChop.ML --- 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"; diff -r fca9cd9fd115 -r 291ce4c4b50e src/HOL/Lex/MaxPrefix.ML --- 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); diff -r fca9cd9fd115 -r 291ce4c4b50e src/HOL/Lex/MaxPrefix.thy --- 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