| products/sources/formale Sprachen/Isabelle/Sequents/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: fspmlp.ML Sprache: IsabelleUntersuchung Isabelle© |
|
||||||
|
(* Title: Sequents/Modal0.thy
Author: Martin Coen Copyright 1991 University of Cambridge *) theory Modal0 imports LK0 begin ML_file \<open>modal.ML\<close> consts box :: "o\ dia :: "o\ Lstar :: "two_seqi" Rstar :: "two_seqi" syntax "_Lstar" :: "two_seqe" ("(_)|L>(_)" [6,6] 5) "_Rstar" :: "two_seqe" ("(_)|R>(_)" [6,6] 5) ML \<open> fun star_tr c [s1, s2] = Const(c, dummyT) $ seq_tr s1 $ seq_tr s2; fun star_tr' c [s1, s2] = Const(c, dummyT) $ seq_tr' s1 $ seq_tr' s2; \<close> parse_translation \<open> [(\<^syntax_const>\<open>_Lstar\<close>, K (star_tr \<^const_syntax>\<open>Lstar\<close>)), (\<^syntax_const>\<open>_Rstar\<close>, K (star_tr \<^const_syntax>\<open>Rstar\<close>))] \<close> print_translation \<open> [(\<^const_syntax>\<open>Lstar\<close>, K (star_tr' \<^syntax_const>\<open>_Lstar\<close>)), (\<^const_syntax>\<open>Rstar\<close>, K (star_tr' \<^syntax_const>\<open>_Rstar\<close>))] \<close> definition strimp :: "[o,o]\ where "P --< Q == [](P \ definition streqv :: "[o,o]\ where "P >-< Q == (P --< Q) \ lemmas rewrite_rls = strimp_def streqv_def lemma iffR: "\ apply (unfold iff_def) apply (assumption | rule conjR impR)+ done lemma iffL: "\ apply (unfold iff_def) apply (assumption | rule conjL impL basic)+ done lemmas safe_rls = basic conjL conjR disjL disjR impL impR notL notR iffL iffR and unsafe_rls = allR exL and bound_rls = allL exR end ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.33Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤ |
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
ZieleEntwicklung einer Software für die statische QuellcodeanalyseBot Zugriff |
