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/HOLCF/IOA/meta_theory/ShortExecutions.thy
changeset 62005 68db98c2cd97
parent 62002 f1599e98c4d0 
--- a/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy	Wed Dec 30 22:09:44 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy	Thu Dec 31 00:07:42 2015 +0100
@@ -221,7 +221,7 @@
                tr = Filter (%a. a:ext A)$sch &
                LastActExtsch A sch"
 
-apply (unfold schedules_def has_schedule_def)
+apply (unfold schedules_def has_schedule_def [abs_def])
 apply auto
 apply (rule_tac x = "filter_act$ (Cut (%a. fst a:ext A) (snd ex))" in exI)
 apply (simp add: executions_def)
isabelle