# HG changeset patch
# User wenzelm
# Date 934834032 -7200
# Node ID e41e64476f9b053689a73db9b84e5a38cc86342a
# Parent  b0198ca6586773b5258f05b0519aa51dc60d7de9
'a list: Nil, Cons;

diff -r b0198ca65867 -r e41e64476f9b src/HOL/Lex/RegExp2NA.thy
--- a/src/HOL/Lex/RegExp2NA.thy	Mon Aug 16 22:04:07 1999 +0200
+++ b/src/HOL/Lex/RegExp2NA.thy	Mon Aug 16 22:07:12 1999 +0200
@@ -12,7 +12,7 @@
 types 'a bitsNA = ('a,bool list)na
 
 syntax "##" :: 'a => 'a list set => 'a list set (infixr 65)
-translations "x ## S" == "op # x `` S"
+translations "x ## S" == "Cons x `` S"
 
 constdefs
  atom  :: 'a => 'a bitsNA
diff -r b0198ca65867 -r e41e64476f9b src/HOL/Lex/RegExp2NAe.thy
--- a/src/HOL/Lex/RegExp2NAe.thy	Mon Aug 16 22:04:07 1999 +0200
+++ b/src/HOL/Lex/RegExp2NAe.thy	Mon Aug 16 22:07:12 1999 +0200
@@ -12,7 +12,7 @@
 types 'a bitsNAe = ('a,bool list)nae
 
 syntax "##" :: 'a => 'a list set => 'a list set (infixr 65)
-translations "x ## S" == "op # x `` S"
+translations "x ## S" == "Cons x `` S"
 
 constdefs
  atom  :: 'a => 'a bitsNAe
diff -r b0198ca65867 -r e41e64476f9b src/HOL/List.ML
--- a/src/HOL/List.ML	Mon Aug 16 22:04:07 1999 +0200
+++ b/src/HOL/List.ML	Mon Aug 16 22:07:12 1999 +0200
@@ -253,18 +253,18 @@
 val list_eq_pattern =
   Thm.read_cterm (Theory.sign_of List.thy) ("(xs::'a list) = ys",HOLogic.boolT);
 
-fun last (cons as Const("List.list.op #",_) $ _ $ xs) =
-      (case xs of Const("List.list.[]",_) => cons | _ => last xs)
+fun last (cons as Const("List.list.Cons",_) $ _ $ xs) =
+      (case xs of Const("List.list.Nil",_) => cons | _ => last xs)
   | last (Const("List.op @",_) $ _ $ ys) = last ys
   | last t = t;
 
-fun list1 (Const("List.list.op #",_) $ _ $ Const("List.list.[]",_)) = true
+fun list1 (Const("List.list.Cons",_) $ _ $ Const("List.list.Nil",_)) = true
   | list1 _ = false;
 
-fun butlast ((cons as Const("List.list.op #",_) $ x) $ xs) =
-      (case xs of Const("List.list.[]",_) => xs | _ => cons $ butlast xs)
+fun butlast ((cons as Const("List.list.Cons",_) $ x) $ xs) =
+      (case xs of Const("List.list.Nil",_) => xs | _ => cons $ butlast xs)
   | butlast ((app as Const("List.op @",_) $ xs) $ ys) = app $ butlast ys
-  | butlast xs = Const("List.list.[]",fastype_of xs);
+  | butlast xs = Const("List.list.Nil",fastype_of xs);
 
 val rearr_tac =
   simp_tac (HOL_basic_ss addsimps [append_assoc,append_Nil,append_Cons]);
diff -r b0198ca65867 -r e41e64476f9b src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Aug 16 22:04:07 1999 +0200
+++ b/src/HOL/List.thy	Mon Aug 16 22:07:12 1999 +0200
@@ -8,7 +8,7 @@
 
 List = Datatype + WF_Rel + NatBin +
 
-datatype 'a list = "[]" ("[]") | "#" 'a ('a list) (infixr 65)
+datatype 'a list = Nil ("[]") | Cons 'a ('a list) (infixr "#" 65)
 
 consts
   "@"         :: ['a list, 'a list] => 'a list            (infixr 65)
diff -r b0198ca65867 -r e41e64476f9b src/HOL/String.thy
--- a/src/HOL/String.thy	Mon Aug 16 22:04:07 1999 +0200
+++ b/src/HOL/String.thy	Mon Aug 16 22:07:12 1999 +0200
@@ -67,11 +67,11 @@
 
   (* strings *)
 
-  fun mk_string [] = Syntax.const Syntax.constrainC $ Syntax.const "[]" $ Syntax.const "string"
-    | mk_string (t :: ts) = Syntax.const "op #" $ t $ mk_string ts;
+  fun mk_string [] = Syntax.const Syntax.constrainC $ Syntax.const "Nil" $ Syntax.const "string"
+    | mk_string (t :: ts) = Syntax.const "Cons" $ t $ mk_string ts;
 
-  fun dest_string (Const ("[]", _)) = []
-    | dest_string (Const ("op #", _) $ c $ cs) = dest_char c :: dest_string cs
+  fun dest_string (Const ("Nil", _)) = []
+    | dest_string (Const ("Cons", _) $ c $ cs) = dest_char c :: dest_string cs
     | dest_string _ = raise Match;
 
 
@@ -79,12 +79,12 @@
         mk_string (map mk_char (Syntax.explode_xstr xstr))
     | string_tr (*"_String"*) ts = raise TERM ("string_tr", ts);
 
-  fun cons_tr' (*"op #"*) [c, cs] =
+  fun cons_tr' (*"Cons"*) [c, cs] =
         Syntax.const "_String" $
           syntax_xstr (Syntax.implode_xstr (dest_char c :: dest_string cs))
-    | cons_tr' (*"op #"*) ts = raise Match;
+    | cons_tr' (*"Cons"*) ts = raise Match;
 
 in
   val parse_translation = [("_Char", char_tr), ("_String", string_tr)];
-  val print_translation = [("Char", char_tr'), ("op #", cons_tr')];
+  val print_translation = [("Char", char_tr'), ("Cons", cons_tr')];
 end;
diff -r b0198ca65867 -r e41e64476f9b src/HOL/TLA/Intensional.thy
--- a/src/HOL/TLA/Intensional.thy	Mon Aug 16 22:04:07 1999 +0200
+++ b/src/HOL/TLA/Intensional.thy	Mon Aug 16 22:07:12 1999 +0200
@@ -130,7 +130,7 @@
   "_liftFinset x" == "_lift2 insert x (_const {})"
   "_liftPair x (_liftargs y z)"       == "_liftPair x (_liftPair y z)"
   "_liftPair"     == "_lift2 Pair"
-  "_liftCons"     == "lift2 (op #)"
+  "_liftCons"     == "lift2 Cons"
   "_liftApp"      == "lift2 (op @)"
   "_liftList (_liftargs x xs)"  == "_liftCons x (_liftList xs)"
   "_liftList x"   == "_liftCons x (_const [])"