# HG changeset patch # User wenzelm # Date 1221679638 -7200 # Node ID 7e14443f2dd6ec44db8740276ebc0815852b84d9 # Parent e1dae766c108d79622bda85d9873567c59105efb use ML_prf within proofs; diff -r e1dae766c108 -r 7e14443f2dd6 src/HOLCF/IOA/NTP/Impl.thy --- a/src/HOLCF/IOA/NTP/Impl.thy Wed Sep 17 21:27:17 2008 +0200 +++ b/src/HOLCF/IOA/NTP/Impl.thy Wed Sep 17 21:27:18 2008 +0200 @@ -199,7 +199,7 @@ txt {* 10 cases. First 4 are simple, since state doesn't change *} -ML_command {* val tac2 = asm_full_simp_tac (ss addsimps [@{thm inv2_def}]) *} + ML_prf {* val tac2 = asm_full_simp_tac (ss addsimps [@{thm inv2_def}]) *} txt {* 10 - 7 *} apply (tactic "EVERY1 [tac2,tac2,tac2,tac2]") @@ -255,7 +255,7 @@ apply (simp (no_asm_simp) add: impl_ioas split del: split_if) apply (induct_tac "a") -ML_command {* val tac3 = asm_full_simp_tac (ss addsimps [@{thm inv3_def}]) *} + ML_prf {* val tac3 = asm_full_simp_tac (ss addsimps [@{thm inv3_def}]) *} txt {* 10 - 8 *} @@ -320,7 +320,7 @@ apply (simp (no_asm_simp) add: impl_ioas split del: split_if) apply (induct_tac "a") -ML_command {* val tac4 = asm_full_simp_tac (ss addsimps [@{thm inv4_def}]) *} + ML_prf {* val tac4 = asm_full_simp_tac (ss addsimps [@{thm inv4_def}]) *} txt {* 10 - 2 *}