src/HOLCF/IOA/meta_theory/SimCorrectness.thy
changeset 39159 0dec18004e75
parent 35174 e15040ae75d7
     1.1 --- a/src/HOLCF/IOA/meta_theory/SimCorrectness.thy	Mon Sep 06 19:11:01 2010 +0200
     1.2 +++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.thy	Mon Sep 06 19:13:10 2010 +0200
     1.3 @@ -171,7 +171,7 @@
     1.4           !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R -->
     1.5               mk_trace C$ex = mk_trace A$((corresp_ex_simC A R$ex) s')"
     1.6  
     1.7 -apply (tactic {* pair_induct_tac @{context} "ex" [thm "is_exec_frag_def"] 1 *})
     1.8 +apply (tactic {* pair_induct_tac @{context} "ex" [@{thm is_exec_frag_def}] 1 *})
     1.9  (* cons case *)
    1.10  apply auto
    1.11  apply (rename_tac ex a t s s')