diff -r 6836da75b3ac -r fa6f654cbc13 thys2/Recs.thy
--- a/thys2/Recs.thy	Thu Jan 10 12:51:24 2019 +0000
+++ b/thys2/Recs.thy	Thu Jan 10 13:00:04 2019 +0000
@@ -1,8 +1,7 @@
 theory Recs
   imports Main
-        "~~/src/HOL/Number_Theory/Primes"  
-        "~~/src/HOL/Library/Nat_Bijection"
-        "~~/src/HOL/Library/Discrete"
+     "~~/src/HOL/Library/Nat_Bijection"
+     "~~/src/HOL/Library/Discrete"
 begin
 
 declare One_nat_def[simp del]
@@ -775,19 +774,19 @@
 
 text {* Membership for the List Encoding *}
 
-fun within :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
-  "within z 0 = (0 < z)"
-| "within z (Suc n) = within (pdec2 z) n"
+fun inside :: "nat \<Rightarrow> nat \<Rightarrow> bool" where
+  "inside z 0 = (0 < z)"
+| "inside z (Suc n) = inside (pdec2 z) n"
     
 definition enclen :: "nat \<Rightarrow> nat" where
-  "enclen z = BMax_rec (\<lambda>x. within z (x - 1)) z"
+  "enclen z = BMax_rec (\<lambda>x. inside z (x - 1)) z"
 
-lemma within_False [simp]:
-  "within 0 n = False"
+lemma inside_False [simp]:
+  "inside 0 n = False"
 by (induct n) (simp_all)
 
-lemma within_length [simp]:
-  "within (lenc xs) s = (s < length xs)"
+lemma inside_length [simp]:
+  "inside (lenc xs) s = (s < length xs)"
 apply(induct s arbitrary: xs)
 apply(case_tac xs)
 apply(simp_all add: prod_encode_def)
@@ -826,17 +825,17 @@
   "rec_ldec = CN rec_predi [CN rec_pdec1 [rec_swap (rec_iter rec_pdec2)]]"
 
 definition 
-  "rec_within = CN rec_less [Z, rec_swap (rec_iter rec_pdec2)]"
+  "rec_inside = CN rec_less [Z, rec_swap (rec_iter rec_pdec2)]"
 
 definition
-  "rec_enclen = CN (rec_max1 (CN rec_not [CN rec_within [Id 2 1, CN rec_predi [Id 2 0]]])) [Id 1 0, Id 1 0]"
+  "rec_enclen = CN (rec_max1 (CN rec_not [CN rec_inside [Id 2 1, CN rec_predi [Id 2 0]]])) [Id 1 0, Id 1 0]"
 
 lemma ldec_iter:
   "ldec z n = pdec1 (Iter pdec2 n z) - 1"
 by (induct n arbitrary: z) (simp | subst Iter_comm)+
 
-lemma within_iter:
-  "within z n = (0 < Iter pdec2 n z)"
+lemma inside_iter:
+  "inside z n = (0 < Iter pdec2 n z)"
 by (induct n arbitrary: z) (simp | subst Iter_comm)+
 
 lemma lenc_lemma [simp]:
@@ -847,9 +846,9 @@
   "rec_eval rec_ldec [z, n] = ldec z n"
 by (simp add: ldec_iter rec_ldec_def)
 
-lemma within_lemma [simp]:
-  "rec_eval rec_within [z, n] = (if within z n then 1 else 0)"
-by (simp add: within_iter rec_within_def)
+lemma inside_lemma [simp]:
+  "rec_eval rec_inside [z, n] = (if inside z n then 1 else 0)"
+by (simp add: inside_iter rec_inside_def)
 
 lemma enclen_lemma [simp]:
   "rec_eval rec_enclen [z] = enclen z"