src/HOLCF/IOA/meta_theory/Seq.ML

--- a/src/HOLCF/IOA/meta_theory/Seq.ML	Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Seq.ML	Wed May 21 15:08:52 1997 +0200
@@ -1,5 +1,5 @@
 (*  Title:      HOLCF/IOA/meta_theory/Seq.ML
-    ID:        
+    ID:         $Id$
     Author:     Olaf M"uller
     Copyright   1996  TU Muenchen
 
@@ -16,6 +16,9 @@
 
 Addsimps [UU_neq_nil];
 
+
+
+
 (* ------------------------------------------------------------------------------------- *)
 
 
@@ -224,7 +227,7 @@
 by (REPEAT (Asm_full_simp_tac 1));
 qed"sconc_cons";
 
-Addsimps [sconc_nil, sconc_UU,sconc_cons];
+Addsimps [sconc_nil,sconc_UU,sconc_cons];
 
 
 (* ----------------------------------------------------------- *)
@@ -311,7 +314,7 @@
 
 (* ------------------------------------------------------------------------------------- *)
 
-section "scons";
+section "scons, nil";
 
 goal thy 
  "!!x. [|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)";
@@ -320,6 +323,15 @@
 auto();
 qed"scons_inject_eq";
 
+goal thy "!!x. nil<<x ==> nil=x";
+by (res_inst_tac [("x","x")] seq.cases 1);
+by (hyp_subst_tac 1);
+by (etac antisym_less 1);
+by (Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
+by (hyp_subst_tac 1);
+by (Asm_full_simp_tac 1);
+qed"nil_less_is_nil";
 
 (* ------------------------------------------------------------------------------------- *)