Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/HoareParallel/Graph.thy
changeset 32442 87d98857d154
parent 31082 54a442b2d727 
--- a/src/HOL/HoareParallel/Graph.thy	Fri Aug 28 20:02:18 2009 +0200
+++ b/src/HOL/HoareParallel/Graph.thy	Fri Aug 28 20:07:11 2009 +0200
@@ -203,11 +203,11 @@
   apply(rule_tac x = "(take m path)@patha" in exI)
   apply(subgoal_tac "\<not>(length path\<le>m)")
    prefer 2 apply arith
-  apply(simp add: min_def)
+  apply(simp)
   apply(rule conjI)
    apply(subgoal_tac "\<not>(m + length patha - 1 < m)")
     prefer 2 apply arith
-   apply(simp add: nth_append min_def)
+   apply(simp add: nth_append)
   apply(rule conjI)
    apply(case_tac "m")
     apply force
@@ -236,7 +236,7 @@
     apply(erule_tac x = "m - 1" in allE)
     apply(simp add: nth_list_update)
    apply(force simp add: nth_list_update)
-  apply(simp add: nth_append min_def)
+  apply(simp add: nth_append)
   apply(rotate_tac -4)
   apply(erule_tac x = "i - m" in allE)
   apply(subgoal_tac "Suc (i - m)=(Suc i - m)" )
@@ -248,8 +248,7 @@
  apply(rule_tac x = "take (Suc m) path" in exI)
  apply(subgoal_tac "\<not>(length path\<le>Suc m)" )
   prefer 2 apply arith
- apply(simp add: min_def)
- apply clarify
+ apply clarsimp
  apply(erule_tac x = "i" in allE)
  apply simp
  apply clarify
isabelle