Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
adapted to new simp lemmas
authornipkow
Sat, 17 Jun 2017 18:49:19 +0200
changeset 66110 d59f9f696110
parent 66109 e034a563ed7d
child 66111 20304512a33b
adapted to new simp lemmas
src/HOL/Bali/Eval.thy file | annotate | diff | comparison | revisions
src/HOL/ex/Bubblesort.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Bali/Eval.thy	Sat Jun 17 15:41:19 2017 +0200
+++ b/src/HOL/Bali/Eval.thy	Sat Jun 17 18:49:19 2017 +0200
@@ -191,7 +191,6 @@
 defer 
 apply (case_tac "a' = Null")
 apply  simp_all
-apply iprover
 done
 
 definition
--- a/src/HOL/ex/Bubblesort.thy	Sat Jun 17 15:41:19 2017 +0200
+++ b/src/HOL/ex/Bubblesort.thy	Sat Jun 17 18:49:19 2017 +0200
@@ -45,7 +45,7 @@
 apply(induction xs rule: bubble_min.induct)
   apply simp
  apply simp
-apply (auto simp: add_eq_conv_ex split: list.split)
+apply (auto split: list.split)
 done
 
 lemma bubble_minD_mset:
isabelle