--- a/src/HOL/HoareParallel/OG_Tactics.thy Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/HoareParallel/OG_Tactics.thy Fri Mar 13 19:58:26 2009 +0100
@@ -465,21 +465,21 @@
Isabelle proofs. *}
method_setup oghoare = {*
- Method.no_args (Method.SIMPLE_METHOD' oghoare_tac) *}
+ Method.no_args (SIMPLE_METHOD' oghoare_tac) *}
"verification condition generator for the oghoare logic"
method_setup annhoare = {*
- Method.no_args (Method.SIMPLE_METHOD' annhoare_tac) *}
+ Method.no_args (SIMPLE_METHOD' annhoare_tac) *}
"verification condition generator for the ann_hoare logic"
method_setup interfree_aux = {*
- Method.no_args (Method.SIMPLE_METHOD' interfree_aux_tac) *}
+ Method.no_args (SIMPLE_METHOD' interfree_aux_tac) *}
"verification condition generator for interference freedom tests"
text {* Tactics useful for dealing with the generated verification conditions: *}
method_setup conjI_tac = {*
- Method.no_args (Method.SIMPLE_METHOD' (conjI_Tac (K all_tac))) *}
+ Method.no_args (SIMPLE_METHOD' (conjI_Tac (K all_tac))) *}
"verification condition generator for interference freedom tests"
ML {*
@@ -490,7 +490,7 @@
*}
method_setup disjE_tac = {*
- Method.no_args (Method.SIMPLE_METHOD' (disjE_Tac (K all_tac))) *}
+ Method.no_args (SIMPLE_METHOD' (disjE_Tac (K all_tac))) *}
"verification condition generator for interference freedom tests"
end