src/Tools/isac/ProgLang/ListC.thy
branchdecompose-isar
changeset 41900 8391d3789efb
parent 41899 d837e83a4835
child 41905 b772eb34c16c
     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