# HG changeset patch
# User paulson
# Date 1101127947 -3600
# Node ID 10dd989282fdebf3d11a169a82ee36bb685e5570
# Parent  51f3d31e8eeaa0dabecd8564781b46492a81118d
indentation

diff -r 51f3d31e8eea -r 10dd989282fd src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Nov 22 11:54:08 2004 +0100
+++ b/src/HOL/List.thy	Mon Nov 22 13:52:27 2004 +0100
@@ -100,93 +100,118 @@
 
 
 primrec
-"hd(x#xs) = x"
+  "hd(x#xs) = x"
+
 primrec
-"tl([]) = []"
-"tl(x#xs) = xs"
+  "tl([]) = []"
+  "tl(x#xs) = xs"
+
 primrec
-"null([]) = True"
-"null(x#xs) = False"
+  "null([]) = True"
+  "null(x#xs) = False"
+
 primrec
-"last(x#xs) = (if xs=[] then x else last xs)"
+  "last(x#xs) = (if xs=[] then x else last xs)"
+
 primrec
-"butlast []= []"
-"butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"
+  "butlast []= []"
+  "butlast(x#xs) = (if xs=[] then [] else x#butlast xs)"
+
 primrec
-"x mem [] = False"
-"x mem (y#ys) = (if y=x then True else x mem ys)"
+  "x mem [] = False"
+  "x mem (y#ys) = (if y=x then True else x mem ys)"
+
 primrec
-"set [] = {}"
-"set (x#xs) = insert x (set xs)"
+  "set [] = {}"
+  "set (x#xs) = insert x (set xs)"
+
 primrec
-list_all_Nil:"list_all P [] = True"
-list_all_Cons: "list_all P (x#xs) = (P(x) \<and> list_all P xs)"
-primrec
-"map f [] = []"
-"map f (x#xs) = f(x)#map f xs"
+  list_all_Nil:"list_all P [] = True"
+  list_all_Cons: "list_all P (x#xs) = (P(x) \<and> list_all P xs)"
+
 primrec
-append_Nil:"[]@ys = ys"
-append_Cons: "(x#xs)@ys = x#(xs@ys)"
+  "map f [] = []"
+  "map f (x#xs) = f(x)#map f xs"
+
 primrec
-"rev([]) = []"
-"rev(x#xs) = rev(xs) @ [x]"
+  append_Nil:"[]@ys = ys"
+  append_Cons: "(x#xs)@ys = x#(xs@ys)"
+
 primrec
-"filter P [] = []"
-"filter P (x#xs) = (if P x then x#filter P xs else filter P xs)"
+  "rev([]) = []"
+  "rev(x#xs) = rev(xs) @ [x]"
+
 primrec
-foldl_Nil:"foldl f a [] = a"
-foldl_Cons: "foldl f a (x#xs) = foldl f (f a x) xs"
+  "filter P [] = []"
+  "filter P (x#xs) = (if P x then x#filter P xs else filter P xs)"
+
 primrec
-"foldr f [] a = a"
-"foldr f (x#xs) a = f x (foldr f xs a)"
+  foldl_Nil:"foldl f a [] = a"
+  foldl_Cons: "foldl f a (x#xs) = foldl f (f a x) xs"
+
 primrec
-"concat([]) = []"
-"concat(x#xs) = x @ concat(xs)"
+  "foldr f [] a = a"
+  "foldr f (x#xs) a = f x (foldr f xs a)"
+
 primrec
-drop_Nil:"drop n [] = []"
-drop_Cons: "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
--- {* Warning: simpset does not contain this definition *}
--- {* but separate theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
+  "concat([]) = []"
+  "concat(x#xs) = x @ concat(xs)"
+
 primrec
-take_Nil:"take n [] = []"
-take_Cons: "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
--- {* Warning: simpset does not contain this definition *}
--- {* but separate theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
+  drop_Nil:"drop n [] = []"
+  drop_Cons: "drop n (x#xs) = (case n of 0 => x#xs | Suc(m) => drop m xs)"
+  -- {*Warning: simpset does not contain this definition, but separate
+       theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
+
 primrec
-nth_Cons:"(x#xs)!n = (case n of 0 => x | (Suc k) => xs!k)"
--- {* Warning: simpset does not contain this definition *}
--- {* but separate theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
+  take_Nil:"take n [] = []"
+  take_Cons: "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
+  -- {*Warning: simpset does not contain this definition, but separate
+       theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
+
 primrec
-"[][i:=v] = []"
-"(x#xs)[i:=v] =
-(case i of 0 => v # xs
-| Suc j => x # xs[j:=v])"
+  nth_Cons:"(x#xs)!n = (case n of 0 => x | (Suc k) => xs!k)"
+  -- {*Warning: simpset does not contain this definition, but separate
+       theorems for @{text "n = 0"} and @{text "n = Suc k"} *}
+
 primrec
-"takeWhile P [] = []"
-"takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"
+  "[][i:=v] = []"
+  "(x#xs)[i:=v] = (case i of 0 => v # xs | Suc j => x # xs[j:=v])"
+
+primrec
+  "takeWhile P [] = []"
+  "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"
+
 primrec
-"dropWhile P [] = []"
-"dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
+  "dropWhile P [] = []"
+  "dropWhile P (x#xs) = (if P x then dropWhile P xs else x#xs)"
+
 primrec
-"zip xs [] = []"
-zip_Cons: "zip xs (y#ys) = (case xs of [] => [] | z#zs => (z,y)#zip zs ys)"
--- {* Warning: simpset does not contain this definition *}
--- {* but separate theorems for @{text "xs = []"} and @{text "xs = z # zs"} *}
+  "zip xs [] = []"
+  zip_Cons: "zip xs (y#ys) = (case xs of [] => [] | z#zs => (z,y)#zip zs ys)"
+  -- {*Warning: simpset does not contain this definition, but separate
+       theorems for @{text "xs = []"} and @{text "xs = z # zs"} *}
+
 primrec
-upt_0: "[i..0(] = []"
-upt_Suc: "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])"
+  upt_0: "[i..0(] = []"
+  upt_Suc: "[i..(Suc j)(] = (if i <= j then [i..j(] @ [j] else [])"
+
 primrec
-"distinct [] = True"
-"distinct (x#xs) = (x ~: set xs \<and> distinct xs)"
+  "distinct [] = True"
+  "distinct (x#xs) = (x ~: set xs \<and> distinct xs)"
+
 primrec
-"remdups [] = []"
-"remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"
+  "remdups [] = []"
+  "remdups (x#xs) = (if x : set xs then remdups xs else x # remdups xs)"
+
 primrec
-"remove1 x [] = []"
-"remove1 x (y#xs) = (if x=y then xs else y # remove1 x xs)"
+  "remove1 x [] = []"
+  "remove1 x (y#xs) = (if x=y then xs else y # remove1 x xs)"
+
 primrec
-replicate_0: "replicate 0 x = []"
-replicate_Suc: "replicate (Suc n) x = x # replicate n x"
+  replicate_0: "replicate 0 x = []"
+  replicate_Suc: "replicate (Suc n) x = x # replicate n x"
+
 defs
 rotate1_def: "rotate1 xs == (case xs of [] \<Rightarrow> [] | x#xs \<Rightarrow> xs @ [x])"
 rotate_def:  "rotate n == rotate1 ^ n"