--- a/src/Doc/Logics_ZF/FOL_examples.thy Tue Jan 16 09:12:16 2018 +0100
+++ b/src/Doc/Logics_ZF/FOL_examples.thy Tue Jan 16 09:30:00 2018 +0100
@@ -3,22 +3,22 @@
theory FOL_examples imports FOL begin
lemma "EX y. ALL x. P(y)-->P(x)"
- \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close>
+ \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rule exCI)
- \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close>
+ \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rule allI)
- \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close>
+ \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rule impI)
- \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close>
+ \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (erule allE)
- \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close>
+ \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
txt\<open>see below for @{text allI} combined with @{text swap}\<close>
apply (erule allI [THEN [2] swap])
- \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close>
+ \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (rule impI)
- \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close>
+ \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply (erule notE)
- \<comment>\<open>@{subgoals[display,indent=0,margin=65]}\<close>
+ \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close>
apply assumption
done