1.1 --- a/src/Tools/isac/ProgLang/ListC.thy	Fri Feb 25 13:26:45 2011 +0100
     1.2 +++ b/src/Tools/isac/ProgLang/ListC.thy	Sat Feb 26 11:34:08 2011 +0100
     1.3 @@ -41,6 +41,7 @@
     1.4    the condition involves another rule set (erls, eval_binop in Atools):*)
     1.5    NTH_CONS:     "1 < n ==> NTH n (x#xs) = NTH (n+ - 1) xs"
     1.6  
     1.7 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
     1.8  (*primrec from Isabelle/src/HOL/List.thy -- def.twice not allowed*)
     1.9  (*primrec*)
    1.10    hd_thm:	"hd(x#xs) = x"
    1.11 @@ -55,9 +56,12 @@
    1.12  (*primrec*)
    1.13    butlast_Nil:	"butlast []    = []"
    1.14    butlast_Cons:	"butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"
    1.15 -(*primrec*)
    1.16 +(*primrec
    1.17    mem_Nil:	"x mem []     = False"
    1.18    mem_Cons:	"x mem (y#ys) = (if y=x then True else x mem ys)"
    1.19 +*)
    1.20 +  mem_Nil:	"x : set []     = False"
    1.21 +  mem_Cons:	"x : set (y#ys) = (if y=x then True else x : set ys)"
    1.22  (*primrec-------already named---
    1.23    "set [] = {}"
    1.24    "set (x#xs) = insert x (set xs)"
    1.25 @@ -194,4 +198,6 @@
    1.26    [("list_rls",list_rls)
    1.27     ]);
    1.28  *}
    1.29 +-.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
    1.30 +
    1.31  end