--- a/src/HOL/BCV/Plus.ML Fri Sep 01 18:01:05 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,48 +0,0 @@
-(* Title: HOL/BCV/Plus.ML
- ID: $Id$
- Author: Tobias Nipkow
- Copyright 1999 TUM
-*)
-
-(** option **)
-
-Goalw [plus_option] "x+None = x";
-by (simp_tac (simpset() addsplits [option.split]) 1);
-qed "plus_None";
-Addsimps [plus_None];
-
-Goalw [plus_option] "None+x = x";
-by (simp_tac (simpset() addsplits [option.split]) 1);
-qed "None_plus";
-Addsimps [None_plus];
-
-Goalw [plus_option] "Some x + Some y = Some(x+y)";
-by (Simp_tac 1);
-qed "Some_plus_Some";
-Addsimps [Some_plus_Some];
-
-Goalw [plus_option] "? y. Some x + opt = Some y";
-by (simp_tac (simpset() addsplits [option.split]) 1);
-qed "plus_option_Some_Some";
-
-(** list **)
-
-Goal "list_plus xs [] = xs";
-by (induct_tac "xs" 1);
- by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsplits [list.split]) 1);
-qed "list_plus_Nil2";
-Addsimps [list_plus_Nil2];
-
-Goal "!ys. length(list_plus xs ys) = max(length xs) (length ys)";
-by (induct_tac "xs" 1);
- by (Simp_tac 1);
-by (asm_simp_tac (simpset() addsplits [list.split]) 1);
-qed_spec_mp "length_list_plus";
-Addsimps [length_list_plus];
-
-Goalw [plus_list]
- "length(ts+us) = max (length ts) (length us)";
-by (Simp_tac 1);
-qed "length_plus_list";
-Addsimps [length_plus_list];