doc-src/ZF/FOL_examples.thy

added type global_theory -- theory or local_theory;
added begin/exit_local_theory;
removed theory_context;
renamed body_context_node to presentation_context;
removed copy (checkpoint twice instead -- avoids unrelated theories);

header{*Examples of Classical Reasoning*}

theory FOL_examples imports FOL begin

lemma "EX y. ALL x. P(y)-->P(x)"
  --{* @{subgoals[display,indent=0,margin=65]} *}
apply (rule exCI)
  --{* @{subgoals[display,indent=0,margin=65]} *}
apply (rule allI)
  --{* @{subgoals[display,indent=0,margin=65]} *}
apply (rule impI)
  --{* @{subgoals[display,indent=0,margin=65]} *}
apply (erule allE)
  --{* @{subgoals[display,indent=0,margin=65]} *}
txt{*see below for @{text allI} combined with @{text swap}*}
apply (erule allI [THEN [2] swap])
  --{* @{subgoals[display,indent=0,margin=65]} *}
apply (rule impI)
  --{* @{subgoals[display,indent=0,margin=65]} *}
apply (erule notE)
  --{* @{subgoals[display,indent=0,margin=65]} *}
apply assumption
done

text {*
@{thm[display] allI [THEN [2] swap]}
*}

lemma "EX y. ALL x. P(y)-->P(x)"
by blast

end