--- a/src/HOL/IMP/VC.thy Sun Dec 09 14:37:42 2001 +0100
+++ b/src/HOL/IMP/VC.thy Sun Dec 09 15:26:13 2001 +0100
@@ -90,7 +90,8 @@
apply fast
done
-lemma awp_mono [rule_format (no_asm)]: "!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp c Q s)"
+lemma awp_mono [rule_format (no_asm)]:
+ "!P Q. (!s. P s --> Q s) --> (!s. awp c P s --> awp c Q s)"
apply (induct_tac "c")
apply (simp_all (no_asm_simp))
apply (rule allI, rule allI, rule impI)
@@ -99,7 +100,8 @@
done
-lemma vc_mono [rule_format (no_asm)]: "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)"
+lemma vc_mono [rule_format (no_asm)]:
+ "!P Q. (!s. P s --> Q s) --> (!s. vc c P s --> vc c Q s)"
apply (induct_tac "c")
apply (simp_all (no_asm_simp))
apply safe