src/Doc/ProgProve/Bool_nat_list.thy
changeset 55320 8a6ee5c1f2e0
parent 55318 908fd015cf2e
child 55465 0d31c0546286
equal deleted inserted replaced
55319:e33f25233798 55320:8a6ee5c1f2e0
   182 "rev (Cons x xs) = app (rev xs) (Cons x Nil)"
   182 "rev (Cons x xs) = app (rev xs) (Cons x Nil)"
   183 
   183 
   184 text{* By default, variables @{text xs}, @{text ys} and @{text zs} are of
   184 text{* By default, variables @{text xs}, @{text ys} and @{text zs} are of
   185 @{text list} type.
   185 @{text list} type.
   186 
   186 
   187 Command \isacom{value}\indexed{{\sf\textbf{value}}}{value} evaluates a term. For example, *}
   187 Command \indexed{\isacommand{value}}{value} evaluates a term. For example, *}
   188 
   188 
   189 value "rev(Cons True (Cons False Nil))"
   189 value "rev(Cons True (Cons False Nil))"
   190 
   190 
   191 text{* yields the result @{value "rev(Cons True (Cons False Nil))"}. This works symbolically, too: *}
   191 text{* yields the result @{value "rev(Cons True (Cons False Nil))"}. This works symbolically, too: *}
   192 
   192