| products/sources/formale sprachen/Isabelle/HOL/Analysis/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Manual_Nits.thy Sprache: IsabelleOriginal von: Isabelle© |
|
||||||
|
section\<open>Examples of Classical Reasoning\<close>
theory FOL_examples imports FOL begin lemma "EX y. ALL x. P(y)-->P(x)" \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> apply (rule exCI) \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> apply (rule allI) \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> apply (rule impI) \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> apply (erule allE) \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> txt\<open>see below for \<open>allI\<close> combined with \<open>swap\<close>\<close> apply (erule allI [THEN [2] swap]) \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> apply (rule impI) \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> apply (erule notE) \<comment> \<open>@{subgoals[display,indent=0,margin=65]}\<close> apply assumption done text \<open> @{thm[display] allI [THEN [2] swap]} \<close> lemma "EX y. ALL x. P(y)-->P(x)" by blast end ¤ Dauer der Verarbeitung: 0.3 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
