--- a/thys/CountSnoc.thy.orig	Tue Oct 07 18:43:29 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,39 +0,0 @@
-theory CountSnoc
-imports Main
-begin
-
-datatype 'a myList = Nil | Cons 'a "'a myList"
-
-fun app_list :: "'a myList \<Rightarrow> 'a myList \<Rightarrow> 'a myList" where
-"app_list Nil ys = ys" |
-"app_list (Cons x xs) ys = Cons x (app_list xs ys)"
-
-fun rev_list :: "'a myList \<Rightarrow> 'a myList" where
-"rev_list Nil = Nil" |
-"rev_list (Cons x xs) = app_list (rev_list xs) (Cons x Nil)"
-
-(*
-fun count_list :: "'a \<Rightarrow> 'a myList \<Rightarrow> nat" where
-"count_list x [] = 0" |
-"count_list x (y#xs) = (
-  if x = y then Suc(count_list x xs) 
-  else count_list x xs)"
-*)
-
-fun count_list :: "'a \<Rightarrow> 'a list \<Rightarrow> nat" where
-"count_list x [] = 0" |
-"count_list x (y#xs) = (
-  if x = y then Suc(count_list x xs) 
-  else count_list x xs)"
-
-<<<<<<< local
-value "count_list 1 [1,1,0]"
-value "count_list 1 [2,2,2]"
-value "count_list 2 [2,2,1]"
-=======
-value "count_list (1::nat) [1,1,1]"
-value "count_list (1::nat) [2,2,2]"
-value "count_list (2::nat) [2,2,1]"
->>>>>>> other
- 
-