doc-src/Intro/list.thy
author blanchet
Fri Apr 30 09:36:45 2010 +0200 (2010-04-30)
changeset 36569 3a29eb7606c3
parent 32960 69916a850301
permissions -rw-r--r--
added "no_atp" for theorems that are automatically used or included by Sledgehammer when appropriate (about combinators and fequal)
     1 List = FOL +
     2 types   list 1
     3 arities list    :: (term)term
     4 consts  Nil     :: "'a list"
     5         Cons    :: "['a, 'a list] => 'a list" 
     6 end