diff --git a/C11-BackEnds/AutoCorres_wrapper/examples/ArrayCmp.thy b/C11-BackEnds/AutoCorres_wrapper/examples/ArrayCmp.thy
new file mode 100644
index 0000000000000000000000000000000000000000..d4128f684b5f37e6412bbb9ddd042abed1766a11
--- /dev/null
+++ b/C11-BackEnds/AutoCorres_wrapper/examples/ArrayCmp.thy
@@ -0,0 +1,72 @@
+(******************************************************************************
+ * Isabelle/C/AutoCorres
+ *
+ * Copyright (c) 2019-2020 Université Paris-Saclay, France
+ *
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ * * Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ *
+ * * Redistributions in binary form must reproduce the above
+ * copyright notice, this list of conditions and the following
+ * disclaimer in the documentation and/or other materials provided
+ * with the distribution.
+ *
+ * * Neither the name of the copyright holders nor the names of its
+ * contributors may be used to endorse or promote products derived
+ * from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ ******************************************************************************)
+
+theory ArrayCmp imports
+ Isabelle_C_AutoCorres.AutoCorres_Wrapper
+begin
+
+
+section\<open>Description\<close>
+
+text\<open>
+The program compares (with respect to the lexicographic order) the subarrays
+with the first n elements of given arrays t1 and t2. The return values are
+\<^enum> 0 if the subarrays are equal,
+\<^enum> 1 if the subarray in t1 is greater than in t2,
+\<^enum> -1 if the subarray in t2 is greater than in t1 \<close>
+
+declare [[AutoCorres]]
+
+C\<open>
+//@ install_autocorres ArrayCmp [heap_abs_syntax]
+
+int ArrayCmp(int n, int* t1, int* t2) {
+ int i;
+ for (i = 0; i < n; i++) {
+ if (t1[i] > t2[i])
+ return -1;
+ else if (t1[i] < t2[i])
+ return 1;
+ }
+ return 0;
+}
+
+\<close>
+
+section\<open>The Proofs (YET TO DO)\<close>
+
+
+end
diff --git a/C11-BackEnds/AutoCorres_wrapper/examples/Check_Subsequence.thy b/C11-BackEnds/AutoCorres_wrapper/examples/Check_Subsequence.thy
new file mode 100644
index 0000000000000000000000000000000000000000..ea0a2f40b6ae227d38f44e83a3b373c21fde1dd8
--- /dev/null
+++ b/C11-BackEnds/AutoCorres_wrapper/examples/Check_Subsequence.thy
@@ -0,0 +1,80 @@
+(******************************************************************************
+ * Isabelle/C/AutoCorres
+ *
+ * Copyright (c) 2019-2020 Université Paris-Saclay, France
+ *
+ * All rights reserved.
+ *
+ * Redistribution and use in source and binary forms, with or without
+ * modification, are permitted provided that the following conditions are
+ * met:
+ *
+ * * Redistributions of source code must retain the above copyright
+ * notice, this list of conditions and the following disclaimer.
+ *
+ * * Redistributions in binary form must reproduce the above
+ * copyright notice, this list of conditions and the following
+ * disclaimer in the documentation and/or other materials provided
+ * with the distribution.
+ *
+ * * Neither the name of the copyright holders nor the names of its
+ * contributors may be used to endorse or promote products derived
+ * from this software without specific prior written permission.
+ *
+ * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+ * "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+ * LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+ * A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+ * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+ * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+ * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+ * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+ * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+ * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+ * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ ******************************************************************************)
+
+theory Check_Subsequence imports
+ Isabelle_C_AutoCorres.AutoCorres_Wrapper
+begin
+
+
+section\<open>Description\<close>
+
+text\<open>
+The program checks if a string array \<open>a\<close> is subsequence of array \<open>b\<close>.
+The strings are expected to termonate by @{C_text \<open>'\0'\<close>}. Return values:
+\<^enum> 0 no substring found, and
+\<^enum> 1 substring test positive.
+\<close>
+
+declare [[AutoCorres]]
+
+C\<open>
+// @ install_autocorres check_subsequence [heap_abs_syntax]
+
+int check_subsequence (char a[], char b[]) {
+ int c, d;
+
+ c = d = 0;
+
+ while (a[c] != '\0') {
+ while ((a[c] != b[d]) && b[d] != '\0') {
+ d++;
+ };
+ if (b[d] == '\0')
+ break;
+ d++;
+ c++;
+ };
+ if (a[c] == '\0')
+ return 1;
+ else
+ return 0;
+}
+\<close>
+
+section\<open>The Proofs (YET TO DO)\<close>
+
+
+end
diff --git a/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_opt2_TCC.thy b/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_opt2_TCC.thy
index a3b47d793f258247e2e6dbb395e3e689512e6f31..34b5784230b306e51667f724eac3fdc9d284efbd 100644
--- a/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_opt2_TCC.thy
+++ b/C11-BackEnds/AutoCorres_wrapper/examples/IsPrime_sqrt_opt2_TCC.thy
@@ -172,10 +172,22 @@ lemma three_is_prime_nat: "prime (3::nat)"
by (metis One_nat_def atLeastLessThan_iff dvd_triv_left even_Suc le_Suc_eq le_def
nat_mult_1_right not_less_eq numeral_2_eq_2 numeral_3_eq_3 prime_nat_numeral_eq set_upt)
+lemma numeral_5_eq_5_nat : "5 = Suc(Suc(Suc(Suc(Suc 0))))"
+ by simp
+
+lemma five_is_prime_nat: "prime (5::nat)"
+ apply(subst numeral_5_eq_5_nat)
+ apply(auto simp: Primes.prime_nat_iff')
+ by (smt Suc_lessI diff_Suc_Suc diff_zero dvd_minus_self linorder_not_le nat_dvd_not_less
+ not_less_eq_eq numeral_2_eq_2)
+
lemma three_and_divides : "prime (p::nat) \<Longrightarrow> 3 < p \<Longrightarrow> \<not>(3 dvd p)"
using primes_dvd_imp_eq three_is_prime_nat by blast
+lemma five_and_divides : "prime (p::nat) \<Longrightarrow> 5 < p \<Longrightarrow> \<not>(5 dvd p)"
+ using primes_dvd_imp_eq three_is_prime_nat
+ by (simp add: prime_nat_not_dvd)
@@ -197,7 +209,7 @@ text\<open> This C code contains a function that determines if the given number
C \<open>
#define SQRT_UINT_MAX 65536
-#define TRUE 1
+#define TRUE 1
#define FALSE 0
unsigned int is_prime(unsigned int n)
@@ -236,81 +248,99 @@ text\<open>This section contains the auxilliary definitions and lemmas for the
final correctness proof; in particular, the loop invariant is stated here.\<close>
-definition is_prime_inv
- where [simp]: "is_prime_inv n i s \<equiv> (5 \<le> i \<and> i \<le> SQRT_UINT_MAX - 1 \<and> i * i \<le> n \<and>
+definition
+is_prime_inv
+ where [simp]: "is_prime_inv n i s \<equiv> (5 \<le> i \<and> i \<le> SQRT_UINT_MAX - 1 \<and> i \<le> n \<and>
(i mod 6) = 5 \<and> partial_prime n i)"
lemma "\<not> 2 dvd i = (i mod 2 = (1::nat))"
using odd_iff_mod_2_eq_one by blast
+lemma simple_binomial : "((a::nat) + b) * (a + b) = a*a + a*b + a*b + b * b"
+ by (simp add: add_mult_distrib2 mult.commute)
lemma inv_preserved0: "is_prime_inv n i s \<Longrightarrow>
\<not> i dvd n \<Longrightarrow> \<not> (i+2) dvd n \<Longrightarrow>
- odd n \<Longrightarrow> \<not> (3 dvd n) \<Longrightarrow>
+ odd n \<Longrightarrow> \<not> (3 dvd n) \<Longrightarrow> 4 < n \<Longrightarrow>
partial_prime n (i + 6)"
unfolding is_prime_inv_def partial_prime_def
-proof(simp, elim conjE)
+proof(elim conjE)
fix i :: nat
assume 1: "odd n"
and 2: "\<not> (3 dvd n)"
- and 2: "i * i \<le> n"
- and 3: "5 \<le> i"
- and 6: "\<forall>i\<in>{2..<min n i}. \<not> i dvd n"
- and 7 :"\<not> i dvd n"
- and 8 :"\<not> (Suc(Suc i)) dvd n"
- and 9: "i mod 6 = 5"
- have 00 :"5 \<le> n"
- by (meson "2" "3" le_square order.trans)
+ and 6: "5 \<le> i"
+ and 7: "\<forall>i\<in>{2..<min n i}. \<not> i dvd n"
+ and 8 :"\<not> i dvd n"
+ and 9 :"\<not> (i + 2) dvd n"
+ and 10 : "i mod 6 = 5"
+ and 100: "4 < n"
+ and 1000: "i \<le> n"
+ have 11 : "\<exists> m::nat. i= m*6+5"
+ by (metis "6" "10" add.commute mod_mod_trivial mult.commute nat_mod_eq_lemma)
+ have ** : "odd i"
+ using "10" by presburger
+ have ***: "\<not>(3 dvd i)"
+ apply(simp add: Rings.semidom_modulo_class.dvd_eq_mod_eq_0)
+ apply(insert 11, erule_tac exE, rename_tac m)
+ by (metis "10" One_nat_def add_Suc_shift gr0I le_add1 le_add_same_cancel1 mod_double_modulus
+ mult_2 numeral_3_eq_3 numeral_Bit0 numeral_eq_iff plus_1_eq_Suc semiring_norm(83)
+ semiring_norm(90) zero_less_numeral )
+ have 12 :"5 \<le> n"
+ using "100" by auto
have *: "\<forall>i\<in>{2..<i}. \<not> i dvd n"
- by (metis "2" "6" le_antisym le_square min_absorb2 min_def order.trans)
- have **: "odd i"
- using "9" by presburger
- have ***: "\<not>(3 dvd i)" sorry
- have ****: "i \<noteq> 0 \<Longrightarrow> \<not>(5 dvd i)" sorry
- have a : "5 * 5 \<le> n"
- by (metis "2" "9" mod_less_eq_dividend mod_mult_mult2 mult_le_mono2 order.trans)
- have *****: "i + 6 < n" sorry
- show "\<forall>i\<in>{2..<min n (i + 6)}. \<not> i dvd n"
- proof (rule ballI, simp, elim conjE)
- fix j :: nat
- assume 10:"j < i + 6"
- and 11 :"2 \<le> j"
- and 12: "j < n"
- show "\<not>(j dvd n)"
- proof(cases "j < i")
- case True
- then show ?thesis
- by (simp add: "*" "11")
- next
- case False
- have "j\<ge>i"
- by (simp add: False le_def)
- have *:"j = i+5 \<or> j = i+4 \<or> j = i+3 \<or> j = i+2 \<or> j = i+1 \<or> j = i "
- using "10" False by linarith
- then show ?thesis
- proof(insert *,elim disjE, simp_all)
- show "\<not> i + 5 dvd n"
- using "**" "1" by auto
- next
- show "\<not> i + 4 dvd n" sledgehammer sorry
- next
- show "\<not> i + 3 dvd n"
- using "**" "1" by auto
- next
- show "\<not> (Suc(Suc i)) dvd n"
- by (simp add: "8")
- next
- show "\<not> (Suc i) dvd n"
- using "**" "1" by auto
- next
- show "\<not> i dvd n"
- by (simp add: "7")
- qed
- qed
+ by (simp add: "1000" "7")
+ show "1 < n \<and> (\<forall>i\<in>{2..<min n (i + 6)}. \<not> i dvd n)"
+ proof(cases "n=5", simp_all)
+ case True
+ then show "\<forall>i\<in>{2..<5}. \<not> i dvd 5"
+ by (metis "*" "6" "8" atLeastLessThan_iff dvd_refl five_is_prime_nat
+ le_neq_implies_less prime_ge_2_nat)
+ next
+ case False
+ assume ** : "n \<noteq> 5"
+ show "Suc 0 < n \<and> (\<forall>i\<in>{2..<min n (i + 6)}. \<not> i dvd n)"
+ apply auto
+ using "100" apply linarith
+ proof (erule contrapos_pp)
+ fix j :: nat
+ assume "2 \<le> j" and "j < n" and "j < i + 6" show "\<not> j dvd n"
+ proof(cases "j < i")
+ case True
+ then show ?thesis
+ by (simp add: "*" \<open>2 \<le> j\<close>)
+ next
+ case False
+ have "j\<ge>i" by (simp add: False le_def)
+ have *:"j = i+5 \<or> j = i+4 \<or> j = i+3 \<or> j = i+2 \<or> j = i+1 \<or> j = i "
+ using False \<open>j < i + 6\<close> by linarith
+
+ then show ?thesis
+ proof(insert *,elim disjE, simp_all)
+ show "\<not> i + 5 dvd n"
+ using "1" "11" by auto
+ next
+ show "\<not> i + 4 dvd n"
+ by (smt "11" "2" Suc_numeral add.assoc add_Suc_right dvd_add_times_triv_left_iff
+ dvd_add_triv_right_iff dvd_refl dvd_trans numeral_3_eq_3 numeral_Bit0
+ numeral_eqs(3) plus_1_eq_Suc semiring_norm(5))
+ next
+ show "\<not> i + 3 dvd n"
+ using "1" "11" by auto
+ next
+ show "\<not> Suc (Suc i) dvd n"
+ using "9" by auto
+ next
+ show "\<not> Suc i dvd n"
+ using "1" "11" by auto
+ next
+ show "\<not> i dvd n"
+ by (simp add: "8")
+ qed
+ qed
+ qed
+ qed
qed
-qed
-
lemma uint_max_factor [simp]: "UINT_MAX = SQRT_UINT_MAX * SQRT_UINT_MAX - 1"
@@ -412,19 +442,95 @@ proof (rule validNF_assume_pre)
then show ?thesis
apply (unfold is_prime'_def dvd_eq_mod_eq_0 [symmetric] SQRT_UINT_MAX_def [symmetric],
insert 1 * **)
- text\<open>... and here happens the annotation with the invariant:
- by instancing @{thm whileLoopE_add_inv}.
- One can say that the while loop is spiced up with the
- invariant and the measure by a rewrite step. \<close>
+ text\<open>... we annotate the loop with the invariant
+ by instancing @{thm whileLoopE_add_inv}. \<close>
apply (subst whileLoopE_add_inv
[ where I = "\<lambda>r s. is_prime_inv n r s"
and M = "\<lambda>(r, s). (Suc n) * (Suc n) - r * r"])
- apply(wp, clarsimp)
- sorry
+ text\<open>... applying vcg and splitting the result: \<close>
+ proof(wp, clarsimp)
+ text\<open>@{term is_prime_inv} holds for loop exits via @{term "return"}.\<close>
+ show "\<lbrace>\<lambda>s. is_prime_inv n 5 s\<rbrace> return (even n \<or> 3 dvd n)
+ \<lbrace>\<lambda>ret s. if ret then (0 \<noteq> 0) = prime n
+ else is_prime_inv n 5 s\<rbrace>!"
+ by(wp, auto simp: ** ***)
+ next
+ text\<open>@{term is_prime_inv} initially holds when entering the loop.\<close>
+ fix s::lifted_globals
+ have **** : "\<not> n < 4 \<Longrightarrow> partial_prime n 5" sorry
+ show "if n < 2 then (0 \<noteq> 0) = prime n
+ else if n < 4 then (1 \<noteq> 0) = prime n
+ else is_prime_inv n 5 s"
+ apply(auto simp: * ****)
+ using not_le prime_ge_2_nat apply auto[1]
+ using "*" less_or_eq_imp_le not_le apply blast
+ using "*" apply linarith
+ apply (simp add: SQRT_UINT_MAX_def)
+ using "*" by linarith
+ next
+ text\<open>@{term is_prime_inv} preserved.\<close>
+ fix r::nat
+ assume "5 \<le> r" and "r \<le> SQRT_UINT_MAX - Suc 0"
+ "r \<le> n" and "r mod 6 = 5" and "partial_prime n r" and
+ "r < 65531" and "r * r \<le> n"
+ show "(r dvd n \<longrightarrow> \<not> prime n) \<and>
+ (Suc (Suc r) dvd n \<longrightarrow> \<not> prime n) \<and>
+ (\<not> r dvd n \<and> \<not> Suc (Suc r) dvd n \<longrightarrow>
+ r + 6 \<le> SQRT_UINT_MAX - Suc 0 \<and>
+ r + 6 \<le> n \<and> partial_prime n (r + 6) \<and> (r < 65525 \<longrightarrow> r + 6 < SQRT_UINT_MAX))"
+ proof(intro conjI impI)
+ show "r dvd n \<Longrightarrow> \<not> prime n"
+ using \<open>5 \<le> r\<close> \<open>r * r \<le> n\<close> prime_dvd by auto
+ next
+ show "Suc (Suc r) dvd n \<Longrightarrow> \<not> prime n"
+ by (smt One_nat_def Suc_leD \<open>5 \<le> r\<close> \<open>r * r \<le> n\<close> dvd_triv_left even_Suc
+ even_mult_iff le_SucE le_antisym le_square less_numeral_extra(3)
+ mult_eq_self_implies_10 nat.inject numeral_eqs(4) prime_dvd zero_less_Suc)
+ next
+ show " r < 65525 \<Longrightarrow> r + 6 < SQRT_UINT_MAX " by(simp add: SQRT_UINT_MAX_def)
+ next
+ assume "\<not> r dvd n \<and> \<not> Suc (Suc r) dvd n"
+ show "partial_prime n (r + 6)"
+ apply(rule inv_preserved0)
+ apply (simp add: \<open>5 \<le> r\<close> \<open>partial_prime n r\<close> \<open>r \<le> SQRT_UINT_MAX - Suc 0\<close>
+ \<open>r \<le> n\<close> \<open>r mod 6 = 5\<close>)
+ apply (simp add: \<open>\<not> r dvd n \<and> \<not> Suc (Suc r) dvd n\<close>)
+ apply (simp add: \<open>\<not> r dvd n \<and> \<not> Suc (Suc r) dvd n\<close>)
+ apply (simp add: "**")
+ apply (simp add: False)
+ by (simp add: "*")
+ next
+ assume "\<not> r dvd n \<and> \<not> Suc (Suc r) dvd n"
+ show "r + 6 \<le> SQRT_UINT_MAX - Suc 0"
+ apply(simp add: SQRT_UINT_MAX_def)
+ apply(insert \<open>r < 65531\<close>)
+ (* feasible : cant be 65530 because even. *)
+ sorry
+ next
+ show "r + 6 \<le> n"
+ apply(insert \<open>r * r \<le> n\<close> \<open>5 \<le> r\<close>)
+ (* feasible : proof below. *)
+ sorry
+ qed
+ next
+ text\<open>@{term is_prime_inv} implies postcond when leaving the loop.\<close>
+ fix r::nat fix s::lifted_globals
+ assume * :"\<not> (r < 65531 \<and> r * r \<le> n)"
+ have ** : "r\<ge>65531 \<or> r * r>n" using "*" leI by blast
+ assume ***: "is_prime_inv n r s"
+ show "((1::nat) \<noteq> 0) = prime n"
+ apply simp
+ apply(case_tac "r\<ge>65531") defer 1
+ using "*" "***" apply auto[1]
+ using "**" partial_prime_sqr apply blast
+ apply(insert ***)
+ (* feasible : between 65531 and 65536 (the integer square of no primes,
+ SQRT_UINT_MAX), there are no primes. *)
+ sorry
+ qed
qed
qed
qed
qed
-
end
diff --git a/README.thy b/README.thy
index 13d01ee178da214a3a0cf5c81b74453a09206073..15284867e6266d9a350f211b247354ee90bf52da 100644
--- a/README.thy
+++ b/README.thy
@@ -69,12 +69,12 @@ Isabelle/C requires Isabelle2019. (This is following the latest version currentl
AutoCorres.)
\<close>
-section \<open>Getting started (for users)\<close>
+section \<open>Getting started (quickstart for users)\<close>
text \<open>
In the sequel, with \<^verbatim>\<open>isabelle\<close> we refer to your local Isabelle2019
-installation, and assume your current working directory is at the root of Isabelle/C (i.e. the
-directory that contains this \<^file>\<open>README.md\<close> file).
+installation, and assume your current working directory is at the root of \<^verbatim>\<open>Isabelle_C\<close>
+(i.e. the directory that contains this \<^file>\<open>README.md\<close> file).
\<^item> Building Isabelle_C :
\<^verbatim>\<open>isabelle build -d\<close> \<^dir>\<open>.\<close> \<^verbatim>\<open>-b Isabelle_C\<close>
@@ -105,11 +105,16 @@ all back-ends enabled is performed with:
text \<open>
The following C examples or entry-points of documentation can be executed:
-\<^item> \<^verbatim>\<open>isabelle jedit -d\<close> \<^dir>\<open>.\<close> \<^file>\<open>C11-FrontEnd/examples/C0.thy\<close>
-\<^item> \<^verbatim>\<open>isabelle jedit -d\<close> \<^dir>\<open>.\<close> \<^file>\<open>C11-FrontEnd/examples/C2.thy\<close>
-\<^item> \<^verbatim>\<open>isabelle jedit -d\<close> \<^dir>\<open>.\<close> \<^file>\<open>C11-FrontEnd/examples/C1.thy\<close>
-\<^item> \<^verbatim>\<open>isabelle jedit -d\<close> \<^dir>\<open>.\<close> \<^file>\<open>C18-FrontEnd/examples/C0.thy\<close>
-\<^item> \<^verbatim>\<open>isabelle jedit -d\<close> \<^dir>\<open>.\<close> \<^file>\<open>C11-FrontEnd/C_Appendices.thy\<close>
+\<^item> \<^verbatim>\<open>isabelle jedit -d\<close> \<^dir>\<open>.\<close> \<^verbatim>\<open>-l Isabelle_C\<close> \<^file>\<open>C11-FrontEnd/examples/C0.thy\<close>
+\<^item> \<^verbatim>\<open>isabelle jedit -d\<close> \<^dir>\<open>.\<close> \<^verbatim>\<open>-l Isabelle_C\<close> \<^file>\<open>C11-FrontEnd/examples/C1.thy\<close>
+\<^item> \<^verbatim>\<open>isabelle jedit -d\<close> \<^dir>\<open>.\<close> \<^verbatim>\<open>-l Isabelle_C\<close> \<^file>\<open>C11-FrontEnd/examples/C2.thy\<close>
+\<^item> \<^verbatim>\<open>isabelle jedit -d\<close> \<^dir>\<open>.\<close> \<^verbatim>\<open>-l Isabelle_C\<close> \<^file>\<open>C18-FrontEnd/examples/C0.thy\<close>
+\<^item> \<^verbatim>\<open>isabelle jedit -d\<close> \<^dir>\<open>.\<close> \<^verbatim>\<open>-l Isabelle_C\<close> \<^file>\<open>C11-FrontEnd/C_Appendices.thy\<close>
+
+The option \<^verbatim>\<open>-l Isabelle_C\<close> can be omitted; it instructs Isabelle to use a
+binary-built version of the \<^verbatim>\<open>Isabelle_C\<close> session. In case of omission,
+Isabelle automatically loads all \<^verbatim>\<open>Isabelle_C\<close> sources, such that the user
+might browse in there or modify any files.
\<close>
text \<open>