1.1 --- a/src/Tools/isac/ProgLang/ListC.thy Sat Feb 26 11:34:08 2011 +0100
1.2 +++ b/src/Tools/isac/ProgLang/ListC.thy Sat Feb 26 12:37:58 2011 +0100
1.3 @@ -41,7 +41,6 @@
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 @@ -198,6 +197,6 @@
1.12 [("list_rls",list_rls)
1.13 ]);
1.14 *}
1.15 +(*-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.
1.16 -.-.-.-.-.-.-isolate response.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.-.*)
1.17 -
1.18 end