equal
deleted
inserted
replaced
104 (* --- Sorting --- *) |
104 (* --- Sorting --- *) |
105 |
105 |
106 Goal "nondec xs --> nondec (oinsert x xs)"; |
106 Goal "nondec xs --> nondec (oinsert x xs)"; |
107 by (induct_tac "xs" 1); |
107 by (induct_tac "xs" 1); |
108 by (case_tac "list" 2); |
108 by (case_tac "list" 2); |
109 by (ALLGOALS (Asm_full_simp_tac)); |
109 by (ALLGOALS(asm_full_simp_tac (simpset()delcongs[thm"list.weak_case_cong"]))); |
110 qed_spec_mp "nondec_oinsert"; |
110 qed_spec_mp "nondec_oinsert"; |
111 |
111 |
112 Goal "nondec (sort xs)"; |
112 Goal "nondec (sort xs)"; |
113 by (induct_tac "xs" 1); |
113 by (induct_tac "xs" 1); |
114 by (ALLGOALS (Asm_full_simp_tac)); |
114 by (ALLGOALS (Asm_full_simp_tac)); |