1.1 --- a/src/Tools/isac/ProgLang/ListC.thy	Wed Dec 02 12:32:30 2020 +0100
     1.2 +++ b/src/Tools/isac/ProgLang/ListC.thy	Mon Dec 07 17:39:21 2020 +0100
     1.3 @@ -60,10 +60,10 @@
     1.4  xfoldr_Nil:  "xfoldr f {|| ||} = id" |
     1.5  xfoldr_Cons: "xfoldr f (x @# xs) = f x \<circ> xfoldr f xs"
     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" |
    1.11 -LENGTH_CONS: "LENGTH (x#xs) = 1 + LENGTH xs"
    1.12 +LENGTH_NIL:	"Length [] = 0" |
    1.13 +LENGTH_CONS: "Length (x#xs) = 1 + Length xs"
    1.14  
    1.15  subsection \<open>Functions for 'list'\<close>
    1.16