Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Lex/MaxPrefix.ML
changeset 10338 291ce4c4b50e
parent 8442 96023903c2df 
--- 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);
isabelle