1.1 --- a/src/Tools/isac/ProgLang/ListC.thy	Wed Sep 08 17:55:08 2010 +0200
     1.2 +++ b/src/Tools/isac/ProgLang/ListC.thy	Thu Sep 09 09:49:14 2010 +0200
     1.3 @@ -16,10 +16,10 @@
     1.4  
     1.5  text {* 'nat' in List.thy replaced by 'real' *}
     1.6  
     1.7 -primrec length_'   :: "'a list => real"
     1.8 +primrec LENGTH   :: "'a list => real"
     1.9  where
    1.10 -  LENGTH_NIL:	"length_' [] = 0"     (*length: 'a list => nat*)
    1.11 -| LENGTH_CONS: "length_' (x#xs) = 1 + length_' xs"
    1.12 +  LENGTH_NIL:	"LENGTH [] = 0"     (*length: 'a list => nat*)
    1.13 +| LENGTH_CONS: "LENGTH (x#xs) = 1 + LENGTH xs"
    1.14  
    1.15  primrec del :: "['a list, 'a] => 'a list"
    1.16  where
    1.17 @@ -31,15 +31,15 @@
    1.18                ("(_ --/ _)" [66, 66] 65)
    1.19    where "a -- b == foldl del a b"
    1.20    
    1.21 -consts nth_' ::  "[real, 'a list] => 'a"
    1.22 +consts NTH ::  "[real, 'a list] => 'a"
    1.23  axioms
    1.24   (*** more than one non-variable in pattern in "nth_ 1 [x] = x"--*)
    1.25 -  NTH_NIL:      "nth_' 1 (x#xs) = x"
    1.26 -(*  NTH_CONS:     "nth_' n (x#xs) = nth_' (n+ -1) xs"  *)
    1.27 +  NTH_NIL:      "NTH 1 (x#xs) = x"
    1.28 +(*  NTH_CONS:     "NTH n (x#xs) = NTH (n+ -1) xs"  *)
    1.29  
    1.30  (*rewriter does not reach base case   ......    ;
    1.31    the condition involves another rule set (erls, eval_binop in Atools):*)
    1.32 -  NTH_CONS:     "1 < n ==> nth_' n (x#xs) = nth_' (n+ - 1) xs"
    1.33 +  NTH_CONS:     "1 < n ==> NTH n (x#xs) = NTH (n+ - 1) xs"
    1.34  
    1.35  (*primrec from Isabelle/src/HOL/List.thy -- def.twice not allowed*)
    1.36  (*primrec*)