# HG changeset patch
# User wenzelm
# Date 1491997687 -7200
# Node ID f3cd78ba687c5c9110c1093776e8bfb811593fe1
# Parent  f556a7a9080ce8a4a878bc54a5e7740b93554791# Parent  104502de757c565ae93e56c737dbb50259e7d729
merged

diff -r f556a7a9080c -r f3cd78ba687c NEWS
--- a/NEWS	Tue Apr 11 10:29:25 2017 +0200
+++ b/NEWS	Wed Apr 12 13:48:07 2017 +0200
@@ -9,6 +9,18 @@
 
 *** General ***
 
+* The main theory entry points for some non-HOL sessions have changed,
+to avoid confusion with the global name "Main" of the session HOL. This
+leads to the follow renamings:
+
+  CTT/Main.thy    ~>  CTT/CTT.thy
+  ZF/Main.thy     ~>  ZF/ZF.thy
+  ZF/Main_ZF.thy  ~>  ZF/ZF.thy
+  ZF/Main_ZFC.thy ~>  ZF/ZFC.thy
+  ZF/ZF.thy       ~>  ZF/ZF_Base.thy
+
+INCOMPATIBILITY.
+
 * Document antiquotations @{prf} and @{full_prf} output proof terms
 (again) in the same way as commands 'prf' and 'full_prf'.
 
@@ -166,6 +178,14 @@
 ISABELLE_PLATFORM64.
 
 
+*** System ***
+
+* System option "record_proofs" allows to change the global
+Proofterm.proofs variable for a session. Regular values are are 0, 1, 2;
+a negative value means the current state in the ML heap image remains
+unchanged.
+
+
 
 New in Isabelle2016-1 (December 2016)
 -------------------------------------
diff -r f556a7a9080c -r f3cd78ba687c etc/options
--- a/etc/options	Tue Apr 11 10:29:25 2017 +0200
+++ b/etc/options	Wed Apr 12 13:48:07 2017 +0200
@@ -82,6 +82,8 @@
 
 section "Detail of Proof Checking"
 
+option record_proofs : int = -1
+  -- "set level of proofterm recording: 0, 1, 2, negative means unchanged"
 option quick_and_dirty : bool = false
   -- "if true then some tools will OMIT some proofs"
 option skip_proofs : bool = false
@@ -111,6 +113,9 @@
 option profiling : string = ""
   -- "ML profiling (possible values: time, allocations)"
 
+option theory_qualifier : string = ""
+  -- "explicit theory qualifier for special sessions (default: session name)"
+
 
 section "ML System"
 
diff -r f556a7a9080c -r f3cd78ba687c src/CTT/Arith.thy
--- a/src/CTT/Arith.thy	Tue Apr 11 10:29:25 2017 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,415 +0,0 @@
-(*  Title:      CTT/Arith.thy
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1991  University of Cambridge
-*)
-
-section \<open>Elementary arithmetic\<close>
-
-theory Arith
-  imports Bool
-begin
-
-subsection \<open>Arithmetic operators and their definitions\<close>
-
-definition add :: "[i,i]\<Rightarrow>i"   (infixr "#+" 65)
-  where "a#+b \<equiv> rec(a, b, \<lambda>u v. succ(v))"
-
-definition diff :: "[i,i]\<Rightarrow>i"   (infixr "-" 65)
-  where "a-b \<equiv> rec(b, a, \<lambda>u v. rec(v, 0, \<lambda>x y. x))"
-
-definition absdiff :: "[i,i]\<Rightarrow>i"   (infixr "|-|" 65)
-  where "a|-|b \<equiv> (a-b) #+ (b-a)"
-
-definition mult :: "[i,i]\<Rightarrow>i"   (infixr "#*" 70)
-  where "a#*b \<equiv> rec(a, 0, \<lambda>u v. b #+ v)"
-
-definition mod :: "[i,i]\<Rightarrow>i"   (infixr "mod" 70)
-  where "a mod b \<equiv> rec(a, 0, \<lambda>u v. rec(succ(v) |-| b, 0, \<lambda>x y. succ(v)))"
-
-definition div :: "[i,i]\<Rightarrow>i"   (infixr "div" 70)
-  where "a div b \<equiv> rec(a, 0, \<lambda>u v. rec(succ(u) mod b, succ(v), \<lambda>x y. v))"
-
-lemmas arith_defs = add_def diff_def absdiff_def mult_def mod_def div_def
-
-
-subsection \<open>Proofs about elementary arithmetic: addition, multiplication, etc.\<close>
-
-subsubsection \<open>Addition\<close>
-
-text \<open>Typing of \<open>add\<close>: short and long versions.\<close>
-
-lemma add_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #+ b : N"
-  unfolding arith_defs by typechk
-
-lemma add_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a #+ b = c #+ d : N"
-  unfolding arith_defs by equal
-
-
-text \<open>Computation for \<open>add\<close>: 0 and successor cases.\<close>
-
-lemma addC0: "b:N \<Longrightarrow> 0 #+ b = b : N"
-  unfolding arith_defs by rew
-
-lemma addC_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a) #+ b = succ(a #+ b) : N"
-  unfolding arith_defs by rew
-
-
-subsubsection \<open>Multiplication\<close>
-
-text \<open>Typing of \<open>mult\<close>: short and long versions.\<close>
-
-lemma mult_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #* b : N"
-  unfolding arith_defs by (typechk add_typing)
-
-lemma mult_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a #* b = c #* d : N"
-  unfolding arith_defs by (equal add_typingL)
-
-
-text \<open>Computation for \<open>mult\<close>: 0 and successor cases.\<close>
-
-lemma multC0: "b:N \<Longrightarrow> 0 #* b = 0 : N"
-  unfolding arith_defs by rew
-
-lemma multC_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a) #* b = b #+ (a #* b) : N"
-  unfolding arith_defs by rew
-
-
-subsubsection \<open>Difference\<close>
-
-text \<open>Typing of difference.\<close>
-
-lemma diff_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a - b : N"
-  unfolding arith_defs by typechk
-
-lemma diff_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a - b = c - d : N"
-  unfolding arith_defs by equal
-
-
-text \<open>Computation for difference: 0 and successor cases.\<close>
-
-lemma diffC0: "a:N \<Longrightarrow> a - 0 = a : N"
-  unfolding arith_defs by rew
-
-text \<open>Note: \<open>rec(a, 0, \<lambda>z w.z)\<close> is \<open>pred(a).\<close>\<close>
-
-lemma diff_0_eq_0: "b:N \<Longrightarrow> 0 - b = 0 : N"
-  unfolding arith_defs
-  apply (NE b)
-    apply hyp_rew
-  done
-
-text \<open>
-  Essential to simplify FIRST!!  (Else we get a critical pair)
-  \<open>succ(a) - succ(b)\<close> rewrites to \<open>pred(succ(a) - b)\<close>.
-\<close>
-lemma diff_succ_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a) - succ(b) = a - b : N"
-  unfolding arith_defs
-  apply hyp_rew
-  apply (NE b)
-    apply hyp_rew
-  done
-
-
-subsection \<open>Simplification\<close>
-
-lemmas arith_typing_rls = add_typing mult_typing diff_typing
-  and arith_congr_rls = add_typingL mult_typingL diff_typingL
-
-lemmas congr_rls = arith_congr_rls intrL2_rls elimL_rls
-
-lemmas arithC_rls =
-  addC0 addC_succ
-  multC0 multC_succ
-  diffC0 diff_0_eq_0 diff_succ_succ
-
-ML \<open>
-  structure Arith_simp = TSimpFun(
-    val refl = @{thm refl_elem}
-    val sym = @{thm sym_elem}
-    val trans = @{thm trans_elem}
-    val refl_red = @{thm refl_red}
-    val trans_red = @{thm trans_red}
-    val red_if_equal = @{thm red_if_equal}
-    val default_rls = @{thms arithC_rls comp_rls}
-    val routine_tac = routine_tac @{thms arith_typing_rls routine_rls}
-  )
-
-  fun arith_rew_tac ctxt prems =
-    make_rew_tac ctxt (Arith_simp.norm_tac ctxt (@{thms congr_rls}, prems))
-
-  fun hyp_arith_rew_tac ctxt prems =
-    make_rew_tac ctxt
-      (Arith_simp.cond_norm_tac ctxt (prove_cond_tac ctxt, @{thms congr_rls}, prems))
-\<close>
-
-method_setup arith_rew = \<open>
-  Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (arith_rew_tac ctxt ths))
-\<close>
-
-method_setup hyp_arith_rew = \<open>
-  Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (hyp_arith_rew_tac ctxt ths))
-\<close>
-
-
-subsection \<open>Addition\<close>
-
-text \<open>Associative law for addition.\<close>
-lemma add_assoc: "\<lbrakk>a:N; b:N; c:N\<rbrakk> \<Longrightarrow> (a #+ b) #+ c = a #+ (b #+ c) : N"
-  apply (NE a)
-    apply hyp_arith_rew
-  done
-
-text \<open>Commutative law for addition.  Can be proved using three inductions.
-  Must simplify after first induction!  Orientation of rewrites is delicate.\<close>
-lemma add_commute: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #+ b = b #+ a : N"
-  apply (NE a)
-    apply hyp_arith_rew
-   apply (rule sym_elem)
-   prefer 2
-   apply (NE b)
-     prefer 4
-     apply (NE b)
-       apply hyp_arith_rew
-  done
-
-
-subsection \<open>Multiplication\<close>
-
-text \<open>Right annihilation in product.\<close>
-lemma mult_0_right: "a:N \<Longrightarrow> a #* 0 = 0 : N"
-  apply (NE a)
-    apply hyp_arith_rew
-  done
-
-text \<open>Right successor law for multiplication.\<close>
-lemma mult_succ_right: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #* succ(b) = a #+ (a #* b) : N"
-  apply (NE a)
-    apply (hyp_arith_rew add_assoc [THEN sym_elem])
-  apply (assumption | rule add_commute mult_typingL add_typingL intrL_rls refl_elem)+
-  done
-
-text \<open>Commutative law for multiplication.\<close>
-lemma mult_commute: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #* b = b #* a : N"
-  apply (NE a)
-    apply (hyp_arith_rew mult_0_right mult_succ_right)
-  done
-
-text \<open>Addition distributes over multiplication.\<close>
-lemma add_mult_distrib: "\<lbrakk>a:N; b:N; c:N\<rbrakk> \<Longrightarrow> (a #+ b) #* c = (a #* c) #+ (b #* c) : N"
-  apply (NE a)
-    apply (hyp_arith_rew add_assoc [THEN sym_elem])
-  done
-
-text \<open>Associative law for multiplication.\<close>
-lemma mult_assoc: "\<lbrakk>a:N; b:N; c:N\<rbrakk> \<Longrightarrow> (a #* b) #* c = a #* (b #* c) : N"
-  apply (NE a)
-    apply (hyp_arith_rew add_mult_distrib)
-  done
-
-
-subsection \<open>Difference\<close>
-
-text \<open>
-  Difference on natural numbers, without negative numbers
-  \<^item> \<open>a - b = 0\<close>  iff  \<open>a \<le> b\<close>
-  \<^item> \<open>a - b = succ(c)\<close> iff \<open>a > b\<close>
-\<close>
-
-lemma diff_self_eq_0: "a:N \<Longrightarrow> a - a = 0 : N"
-  apply (NE a)
-    apply hyp_arith_rew
-  done
-
-
-lemma add_0_right: "\<lbrakk>c : N; 0 : N; c : N\<rbrakk> \<Longrightarrow> c #+ 0 = c : N"
-  by (rule addC0 [THEN [3] add_commute [THEN trans_elem]])
-
-text \<open>
-  Addition is the inverse of subtraction: if \<open>b \<le> x\<close> then \<open>b #+ (x - b) = x\<close>.
-  An example of induction over a quantified formula (a product).
-  Uses rewriting with a quantified, implicative inductive hypothesis.
-\<close>
-schematic_goal add_diff_inverse_lemma:
-  "b:N \<Longrightarrow> ?a : \<Prod>x:N. Eq(N, b-x, 0) \<longrightarrow> Eq(N, b #+ (x-b), x)"
-  apply (NE b)
-    \<comment> \<open>strip one "universal quantifier" but not the "implication"\<close>
-    apply (rule_tac [3] intr_rls)
-    \<comment> \<open>case analysis on \<open>x\<close> in \<open>succ(u) \<le> x \<longrightarrow> succ(u) #+ (x - succ(u)) = x\<close>\<close>
-     prefer 4
-     apply (NE x)
-       apply assumption
-    \<comment> \<open>Prepare for simplification of types -- the antecedent \<open>succ(u) \<le> x\<close>\<close>
-      apply (rule_tac [2] replace_type)
-       apply (rule_tac [1] replace_type)
-        apply arith_rew
-    \<comment> \<open>Solves first 0 goal, simplifies others.  Two sugbgoals remain.
-    Both follow by rewriting, (2) using quantified induction hyp.\<close>
-   apply intr \<comment> \<open>strips remaining \<open>\<Prod>\<close>s\<close>
-    apply (hyp_arith_rew add_0_right)
-  apply assumption
-  done
-
-text \<open>
-  Version of above with premise \<open>b - a = 0\<close> i.e. \<open>a \<ge> b\<close>.
-  Using @{thm ProdE} does not work -- for \<open>?B(?a)\<close> is ambiguous.
-  Instead, @{thm add_diff_inverse_lemma} states the desired induction scheme;
-  the use of \<open>THEN\<close> below instantiates Vars in @{thm ProdE} automatically.
-\<close>
-lemma add_diff_inverse: "\<lbrakk>a:N; b:N; b - a = 0 : N\<rbrakk> \<Longrightarrow> b #+ (a-b) = a : N"
-  apply (rule EqE)
-  apply (rule add_diff_inverse_lemma [THEN ProdE, THEN ProdE])
-    apply (assumption | rule EqI)+
-  done
-
-
-subsection \<open>Absolute difference\<close>
-
-text \<open>Typing of absolute difference: short and long versions.\<close>
-
-lemma absdiff_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a |-| b : N"
-  unfolding arith_defs by typechk
-
-lemma absdiff_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a |-| b = c |-| d : N"
-  unfolding arith_defs by equal
-
-lemma absdiff_self_eq_0: "a:N \<Longrightarrow> a |-| a = 0 : N"
-  unfolding absdiff_def by (arith_rew diff_self_eq_0)
-
-lemma absdiffC0: "a:N \<Longrightarrow> 0 |-| a = a : N"
-  unfolding absdiff_def by hyp_arith_rew
-
-lemma absdiff_succ_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a) |-| succ(b)  =  a |-| b : N"
-  unfolding absdiff_def by hyp_arith_rew
-
-text \<open>Note how easy using commutative laws can be?  ...not always...\<close>
-lemma absdiff_commute: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a |-| b = b |-| a : N"
-  unfolding absdiff_def
-  apply (rule add_commute)
-   apply (typechk diff_typing)
-  done
-
-text \<open>If \<open>a + b = 0\<close> then \<open>a = 0\<close>. Surprisingly tedious.\<close>
-schematic_goal add_eq0_lemma: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> ?c : Eq(N,a#+b,0) \<longrightarrow> Eq(N,a,0)"
-  apply (NE a)
-    apply (rule_tac [3] replace_type)
-     apply arith_rew
-  apply intr  \<comment> \<open>strips remaining \<open>\<Prod>\<close>s\<close>
-   apply (rule_tac [2] zero_ne_succ [THEN FE])
-     apply (erule_tac [3] EqE [THEN sym_elem])
-    apply (typechk add_typing)
-  done
-
-text \<open>
-  Version of above with the premise \<open>a + b = 0\<close>.
-  Again, resolution instantiates variables in @{thm ProdE}.
-\<close>
-lemma add_eq0: "\<lbrakk>a:N; b:N; a #+ b = 0 : N\<rbrakk> \<Longrightarrow> a = 0 : N"
-  apply (rule EqE)
-  apply (rule add_eq0_lemma [THEN ProdE])
-    apply (rule_tac [3] EqI)
-    apply typechk
-  done
-
-text \<open>Here is a lemma to infer \<open>a - b = 0\<close> and \<open>b - a = 0\<close> from \<open>a |-| b = 0\<close>, below.\<close>
-schematic_goal absdiff_eq0_lem:
-  "\<lbrakk>a:N; b:N; a |-| b = 0 : N\<rbrakk> \<Longrightarrow> ?a : Eq(N, a-b, 0) \<times> Eq(N, b-a, 0)"
-  apply (unfold absdiff_def)
-  apply intr
-   apply eqintr
-   apply (rule_tac [2] add_eq0)
-     apply (rule add_eq0)
-       apply (rule_tac [6] add_commute [THEN trans_elem])
-         apply (typechk diff_typing)
-  done
-
-text \<open>If \<open>a |-| b = 0\<close> then \<open>a = b\<close>
-  proof: \<open>a - b = 0\<close> and \<open>b - a = 0\<close>, so \<open>b = a + (b - a) = a + 0 = a\<close>.
-\<close>
-lemma absdiff_eq0: "\<lbrakk>a |-| b = 0 : N; a:N; b:N\<rbrakk> \<Longrightarrow> a = b : N"
-  apply (rule EqE)
-  apply (rule absdiff_eq0_lem [THEN SumE])
-     apply eqintr
-  apply (rule add_diff_inverse [THEN sym_elem, THEN trans_elem])
-     apply (erule_tac [3] EqE)
-    apply (hyp_arith_rew add_0_right)
-  done
-
-
-subsection \<open>Remainder and Quotient\<close>
-
-text \<open>Typing of remainder: short and long versions.\<close>
-
-lemma mod_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a mod b : N"
-  unfolding mod_def by (typechk absdiff_typing)
-
-lemma mod_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a mod b = c mod d : N"
-  unfolding mod_def by (equal absdiff_typingL)
-
-
-text \<open>Computation for \<open>mod\<close>: 0 and successor cases.\<close>
-
-lemma modC0: "b:N \<Longrightarrow> 0 mod b = 0 : N"
-  unfolding mod_def by (rew absdiff_typing)
-
-lemma modC_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow>
-  succ(a) mod b = rec(succ(a mod b) |-| b, 0, \<lambda>x y. succ(a mod b)) : N"
-  unfolding mod_def by (rew absdiff_typing)
-
-
-text \<open>Typing of quotient: short and long versions.\<close>
-
-lemma div_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a div b : N"
-  unfolding div_def by (typechk absdiff_typing mod_typing)
-
-lemma div_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a div b = c div d : N"
-  unfolding div_def by (equal absdiff_typingL mod_typingL)
-
-lemmas div_typing_rls = mod_typing div_typing absdiff_typing
-
-
-text \<open>Computation for quotient: 0 and successor cases.\<close>
-
-lemma divC0: "b:N \<Longrightarrow> 0 div b = 0 : N"
-  unfolding div_def by (rew mod_typing absdiff_typing)
-
-lemma divC_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow>
-  succ(a) div b = rec(succ(a) mod b, succ(a div b), \<lambda>x y. a div b) : N"
-  unfolding div_def by (rew mod_typing)
-
-
-text \<open>Version of above with same condition as the \<open>mod\<close> one.\<close>
-lemma divC_succ2: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow>
-  succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), \<lambda>x y. a div b) : N"
-  apply (rule divC_succ [THEN trans_elem])
-    apply (rew div_typing_rls modC_succ)
-  apply (NE "succ (a mod b) |-|b")
-    apply (rew mod_typing div_typing absdiff_typing)
-  done
-
-text \<open>For case analysis on whether a number is 0 or a successor.\<close>
-lemma iszero_decidable: "a:N \<Longrightarrow> rec(a, inl(eq), \<lambda>ka kb. inr(<ka, eq>)) :
-  Eq(N,a,0) + (\<Sum>x:N. Eq(N,a, succ(x)))"
-  apply (NE a)
-    apply (rule_tac [3] PlusI_inr)
-     apply (rule_tac [2] PlusI_inl)
-      apply eqintr
-     apply equal
-  done
-
-text \<open>Main Result. Holds when \<open>b\<close> is 0 since \<open>a mod 0 = a\<close> and \<open>a div 0 = 0\<close>.\<close>
-lemma mod_div_equality: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a mod b #+ (a div b) #* b = a : N"
-  apply (NE a)
-    apply (arith_rew div_typing_rls modC0 modC_succ divC0 divC_succ2)
-  apply (rule EqE)
-    \<comment> \<open>case analysis on \<open>succ(u mod b) |-| b\<close>\<close>
-  apply (rule_tac a1 = "succ (u mod b) |-| b" in iszero_decidable [THEN PlusE])
-    apply (erule_tac [3] SumE)
-    apply (hyp_arith_rew div_typing_rls modC0 modC_succ divC0 divC_succ2)
-    \<comment> \<open>Replace one occurrence of \<open>b\<close> by \<open>succ(u mod b)\<close>. Clumsy!\<close>
-  apply (rule add_typingL [THEN trans_elem])
-    apply (erule EqE [THEN absdiff_eq0, THEN sym_elem])
-     apply (rule_tac [3] refl_elem)
-     apply (hyp_arith_rew div_typing_rls)
-  done
-
-end
diff -r f556a7a9080c -r f3cd78ba687c src/CTT/Bool.thy
--- a/src/CTT/Bool.thy	Tue Apr 11 10:29:25 2017 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,73 +0,0 @@
-(*  Title:      CTT/Bool.thy
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   1991  University of Cambridge
-*)
-
-section \<open>The two-element type (booleans and conditionals)\<close>
-
-theory Bool
-  imports CTT
-begin
-
-definition Bool :: "t"
-  where "Bool \<equiv> T+T"
-
-definition true :: "i"
-  where "true \<equiv> inl(tt)"
-
-definition false :: "i"
-  where "false \<equiv> inr(tt)"
-
-definition cond :: "[i,i,i]\<Rightarrow>i"
-  where "cond(a,b,c) \<equiv> when(a, \<lambda>_. b, \<lambda>_. c)"
-
-lemmas bool_defs = Bool_def true_def false_def cond_def
-
-
-subsection \<open>Derivation of rules for the type \<open>Bool\<close>\<close>
-
-text \<open>Formation rule.\<close>
-lemma boolF: "Bool type"
-  unfolding bool_defs by typechk
-
-text \<open>Introduction rules for \<open>true\<close>, \<open>false\<close>.\<close>
-
-lemma boolI_true: "true : Bool"
-  unfolding bool_defs by typechk
-
-lemma boolI_false: "false : Bool"
-  unfolding bool_defs by typechk
-
-text \<open>Elimination rule: typing of \<open>cond\<close>.\<close>
-lemma boolE: "\<lbrakk>p:Bool; a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(p,a,b) : C(p)"
-  unfolding bool_defs
-  apply (typechk; erule TE)
-   apply typechk
-  done
-
-lemma boolEL: "\<lbrakk>p = q : Bool; a = c : C(true); b = d : C(false)\<rbrakk>
-  \<Longrightarrow> cond(p,a,b) = cond(q,c,d) : C(p)"
-  unfolding bool_defs
-  apply (rule PlusEL)
-    apply (erule asm_rl refl_elem [THEN TEL])+
-  done
-
-text \<open>Computation rules for \<open>true\<close>, \<open>false\<close>.\<close>
-
-lemma boolC_true: "\<lbrakk>a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(true,a,b) = a : C(true)"
-  unfolding bool_defs
-  apply (rule comp_rls)
-    apply typechk
-   apply (erule_tac [!] TE)
-   apply typechk
-  done
-
-lemma boolC_false: "\<lbrakk>a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(false,a,b) = b : C(false)"
-  unfolding bool_defs
-  apply (rule comp_rls)
-    apply typechk
-   apply (erule_tac [!] TE)
-   apply typechk
-  done
-
-end
diff -r f556a7a9080c -r f3cd78ba687c src/CTT/CTT.thy
--- a/src/CTT/CTT.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/CTT/CTT.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -3,12 +3,12 @@
     Copyright   1993  University of Cambridge
 *)
 
-section \<open>Constructive Type Theory\<close>
-
 theory CTT
 imports Pure
 begin
 
+section \<open>Constructive Type Theory: axiomatic basis\<close>
+
 ML_file "~~/src/Provers/typedsimp.ML"
 setup Pure_Thy.old_appl_syntax_setup
 
@@ -482,4 +482,473 @@
       apply (typechk assms)
   done
 
+
+section \<open>The two-element type (booleans and conditionals)\<close>
+
+definition Bool :: "t"
+  where "Bool \<equiv> T+T"
+
+definition true :: "i"
+  where "true \<equiv> inl(tt)"
+
+definition false :: "i"
+  where "false \<equiv> inr(tt)"
+
+definition cond :: "[i,i,i]\<Rightarrow>i"
+  where "cond(a,b,c) \<equiv> when(a, \<lambda>_. b, \<lambda>_. c)"
+
+lemmas bool_defs = Bool_def true_def false_def cond_def
+
+
+subsection \<open>Derivation of rules for the type \<open>Bool\<close>\<close>
+
+text \<open>Formation rule.\<close>
+lemma boolF: "Bool type"
+  unfolding bool_defs by typechk
+
+text \<open>Introduction rules for \<open>true\<close>, \<open>false\<close>.\<close>
+
+lemma boolI_true: "true : Bool"
+  unfolding bool_defs by typechk
+
+lemma boolI_false: "false : Bool"
+  unfolding bool_defs by typechk
+
+text \<open>Elimination rule: typing of \<open>cond\<close>.\<close>
+lemma boolE: "\<lbrakk>p:Bool; a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(p,a,b) : C(p)"
+  unfolding bool_defs
+  apply (typechk; erule TE)
+   apply typechk
+  done
+
+lemma boolEL: "\<lbrakk>p = q : Bool; a = c : C(true); b = d : C(false)\<rbrakk>
+  \<Longrightarrow> cond(p,a,b) = cond(q,c,d) : C(p)"
+  unfolding bool_defs
+  apply (rule PlusEL)
+    apply (erule asm_rl refl_elem [THEN TEL])+
+  done
+
+text \<open>Computation rules for \<open>true\<close>, \<open>false\<close>.\<close>
+
+lemma boolC_true: "\<lbrakk>a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(true,a,b) = a : C(true)"
+  unfolding bool_defs
+  apply (rule comp_rls)
+    apply typechk
+   apply (erule_tac [!] TE)
+   apply typechk
+  done
+
+lemma boolC_false: "\<lbrakk>a : C(true); b : C(false)\<rbrakk> \<Longrightarrow> cond(false,a,b) = b : C(false)"
+  unfolding bool_defs
+  apply (rule comp_rls)
+    apply typechk
+   apply (erule_tac [!] TE)
+   apply typechk
+  done
+
+section \<open>Elementary arithmetic\<close>
+
+subsection \<open>Arithmetic operators and their definitions\<close>
+
+definition add :: "[i,i]\<Rightarrow>i"   (infixr "#+" 65)
+  where "a#+b \<equiv> rec(a, b, \<lambda>u v. succ(v))"
+
+definition diff :: "[i,i]\<Rightarrow>i"   (infixr "-" 65)
+  where "a-b \<equiv> rec(b, a, \<lambda>u v. rec(v, 0, \<lambda>x y. x))"
+
+definition absdiff :: "[i,i]\<Rightarrow>i"   (infixr "|-|" 65)
+  where "a|-|b \<equiv> (a-b) #+ (b-a)"
+
+definition mult :: "[i,i]\<Rightarrow>i"   (infixr "#*" 70)
+  where "a#*b \<equiv> rec(a, 0, \<lambda>u v. b #+ v)"
+
+definition mod :: "[i,i]\<Rightarrow>i"   (infixr "mod" 70)
+  where "a mod b \<equiv> rec(a, 0, \<lambda>u v. rec(succ(v) |-| b, 0, \<lambda>x y. succ(v)))"
+
+definition div :: "[i,i]\<Rightarrow>i"   (infixr "div" 70)
+  where "a div b \<equiv> rec(a, 0, \<lambda>u v. rec(succ(u) mod b, succ(v), \<lambda>x y. v))"
+
+lemmas arith_defs = add_def diff_def absdiff_def mult_def mod_def div_def
+
+
+subsection \<open>Proofs about elementary arithmetic: addition, multiplication, etc.\<close>
+
+subsubsection \<open>Addition\<close>
+
+text \<open>Typing of \<open>add\<close>: short and long versions.\<close>
+
+lemma add_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #+ b : N"
+  unfolding arith_defs by typechk
+
+lemma add_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a #+ b = c #+ d : N"
+  unfolding arith_defs by equal
+
+
+text \<open>Computation for \<open>add\<close>: 0 and successor cases.\<close>
+
+lemma addC0: "b:N \<Longrightarrow> 0 #+ b = b : N"
+  unfolding arith_defs by rew
+
+lemma addC_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a) #+ b = succ(a #+ b) : N"
+  unfolding arith_defs by rew
+
+
+subsubsection \<open>Multiplication\<close>
+
+text \<open>Typing of \<open>mult\<close>: short and long versions.\<close>
+
+lemma mult_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #* b : N"
+  unfolding arith_defs by (typechk add_typing)
+
+lemma mult_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a #* b = c #* d : N"
+  unfolding arith_defs by (equal add_typingL)
+
+
+text \<open>Computation for \<open>mult\<close>: 0 and successor cases.\<close>
+
+lemma multC0: "b:N \<Longrightarrow> 0 #* b = 0 : N"
+  unfolding arith_defs by rew
+
+lemma multC_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a) #* b = b #+ (a #* b) : N"
+  unfolding arith_defs by rew
+
+
+subsubsection \<open>Difference\<close>
+
+text \<open>Typing of difference.\<close>
+
+lemma diff_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a - b : N"
+  unfolding arith_defs by typechk
+
+lemma diff_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a - b = c - d : N"
+  unfolding arith_defs by equal
+
+
+text \<open>Computation for difference: 0 and successor cases.\<close>
+
+lemma diffC0: "a:N \<Longrightarrow> a - 0 = a : N"
+  unfolding arith_defs by rew
+
+text \<open>Note: \<open>rec(a, 0, \<lambda>z w.z)\<close> is \<open>pred(a).\<close>\<close>
+
+lemma diff_0_eq_0: "b:N \<Longrightarrow> 0 - b = 0 : N"
+  unfolding arith_defs
+  apply (NE b)
+    apply hyp_rew
+  done
+
+text \<open>
+  Essential to simplify FIRST!!  (Else we get a critical pair)
+  \<open>succ(a) - succ(b)\<close> rewrites to \<open>pred(succ(a) - b)\<close>.
+\<close>
+lemma diff_succ_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a) - succ(b) = a - b : N"
+  unfolding arith_defs
+  apply hyp_rew
+  apply (NE b)
+    apply hyp_rew
+  done
+
+
+subsection \<open>Simplification\<close>
+
+lemmas arith_typing_rls = add_typing mult_typing diff_typing
+  and arith_congr_rls = add_typingL mult_typingL diff_typingL
+
+lemmas congr_rls = arith_congr_rls intrL2_rls elimL_rls
+
+lemmas arithC_rls =
+  addC0 addC_succ
+  multC0 multC_succ
+  diffC0 diff_0_eq_0 diff_succ_succ
+
+ML \<open>
+  structure Arith_simp = TSimpFun(
+    val refl = @{thm refl_elem}
+    val sym = @{thm sym_elem}
+    val trans = @{thm trans_elem}
+    val refl_red = @{thm refl_red}
+    val trans_red = @{thm trans_red}
+    val red_if_equal = @{thm red_if_equal}
+    val default_rls = @{thms arithC_rls comp_rls}
+    val routine_tac = routine_tac @{thms arith_typing_rls routine_rls}
+  )
+
+  fun arith_rew_tac ctxt prems =
+    make_rew_tac ctxt (Arith_simp.norm_tac ctxt (@{thms congr_rls}, prems))
+
+  fun hyp_arith_rew_tac ctxt prems =
+    make_rew_tac ctxt
+      (Arith_simp.cond_norm_tac ctxt (prove_cond_tac ctxt, @{thms congr_rls}, prems))
+\<close>
+
+method_setup arith_rew = \<open>
+  Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (arith_rew_tac ctxt ths))
+\<close>
+
+method_setup hyp_arith_rew = \<open>
+  Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD (hyp_arith_rew_tac ctxt ths))
+\<close>
+
+
+subsection \<open>Addition\<close>
+
+text \<open>Associative law for addition.\<close>
+lemma add_assoc: "\<lbrakk>a:N; b:N; c:N\<rbrakk> \<Longrightarrow> (a #+ b) #+ c = a #+ (b #+ c) : N"
+  apply (NE a)
+    apply hyp_arith_rew
+  done
+
+text \<open>Commutative law for addition.  Can be proved using three inductions.
+  Must simplify after first induction!  Orientation of rewrites is delicate.\<close>
+lemma add_commute: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #+ b = b #+ a : N"
+  apply (NE a)
+    apply hyp_arith_rew
+   apply (rule sym_elem)
+   prefer 2
+   apply (NE b)
+     prefer 4
+     apply (NE b)
+       apply hyp_arith_rew
+  done
+
+
+subsection \<open>Multiplication\<close>
+
+text \<open>Right annihilation in product.\<close>
+lemma mult_0_right: "a:N \<Longrightarrow> a #* 0 = 0 : N"
+  apply (NE a)
+    apply hyp_arith_rew
+  done
+
+text \<open>Right successor law for multiplication.\<close>
+lemma mult_succ_right: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #* succ(b) = a #+ (a #* b) : N"
+  apply (NE a)
+    apply (hyp_arith_rew add_assoc [THEN sym_elem])
+  apply (assumption | rule add_commute mult_typingL add_typingL intrL_rls refl_elem)+
+  done
+
+text \<open>Commutative law for multiplication.\<close>
+lemma mult_commute: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a #* b = b #* a : N"
+  apply (NE a)
+    apply (hyp_arith_rew mult_0_right mult_succ_right)
+  done
+
+text \<open>Addition distributes over multiplication.\<close>
+lemma add_mult_distrib: "\<lbrakk>a:N; b:N; c:N\<rbrakk> \<Longrightarrow> (a #+ b) #* c = (a #* c) #+ (b #* c) : N"
+  apply (NE a)
+    apply (hyp_arith_rew add_assoc [THEN sym_elem])
+  done
+
+text \<open>Associative law for multiplication.\<close>
+lemma mult_assoc: "\<lbrakk>a:N; b:N; c:N\<rbrakk> \<Longrightarrow> (a #* b) #* c = a #* (b #* c) : N"
+  apply (NE a)
+    apply (hyp_arith_rew add_mult_distrib)
+  done
+
+
+subsection \<open>Difference\<close>
+
+text \<open>
+  Difference on natural numbers, without negative numbers
+  \<^item> \<open>a - b = 0\<close>  iff  \<open>a \<le> b\<close>
+  \<^item> \<open>a - b = succ(c)\<close> iff \<open>a > b\<close>
+\<close>
+
+lemma diff_self_eq_0: "a:N \<Longrightarrow> a - a = 0 : N"
+  apply (NE a)
+    apply hyp_arith_rew
+  done
+
+
+lemma add_0_right: "\<lbrakk>c : N; 0 : N; c : N\<rbrakk> \<Longrightarrow> c #+ 0 = c : N"
+  by (rule addC0 [THEN [3] add_commute [THEN trans_elem]])
+
+text \<open>
+  Addition is the inverse of subtraction: if \<open>b \<le> x\<close> then \<open>b #+ (x - b) = x\<close>.
+  An example of induction over a quantified formula (a product).
+  Uses rewriting with a quantified, implicative inductive hypothesis.
+\<close>
+schematic_goal add_diff_inverse_lemma:
+  "b:N \<Longrightarrow> ?a : \<Prod>x:N. Eq(N, b-x, 0) \<longrightarrow> Eq(N, b #+ (x-b), x)"
+  apply (NE b)
+    \<comment> \<open>strip one "universal quantifier" but not the "implication"\<close>
+    apply (rule_tac [3] intr_rls)
+    \<comment> \<open>case analysis on \<open>x\<close> in \<open>succ(u) \<le> x \<longrightarrow> succ(u) #+ (x - succ(u)) = x\<close>\<close>
+     prefer 4
+     apply (NE x)
+       apply assumption
+    \<comment> \<open>Prepare for simplification of types -- the antecedent \<open>succ(u) \<le> x\<close>\<close>
+      apply (rule_tac [2] replace_type)
+       apply (rule_tac [1] replace_type)
+        apply arith_rew
+    \<comment> \<open>Solves first 0 goal, simplifies others.  Two sugbgoals remain.
+    Both follow by rewriting, (2) using quantified induction hyp.\<close>
+   apply intr \<comment> \<open>strips remaining \<open>\<Prod>\<close>s\<close>
+    apply (hyp_arith_rew add_0_right)
+  apply assumption
+  done
+
+text \<open>
+  Version of above with premise \<open>b - a = 0\<close> i.e. \<open>a \<ge> b\<close>.
+  Using @{thm ProdE} does not work -- for \<open>?B(?a)\<close> is ambiguous.
+  Instead, @{thm add_diff_inverse_lemma} states the desired induction scheme;
+  the use of \<open>THEN\<close> below instantiates Vars in @{thm ProdE} automatically.
+\<close>
+lemma add_diff_inverse: "\<lbrakk>a:N; b:N; b - a = 0 : N\<rbrakk> \<Longrightarrow> b #+ (a-b) = a : N"
+  apply (rule EqE)
+  apply (rule add_diff_inverse_lemma [THEN ProdE, THEN ProdE])
+    apply (assumption | rule EqI)+
+  done
+
+
+subsection \<open>Absolute difference\<close>
+
+text \<open>Typing of absolute difference: short and long versions.\<close>
+
+lemma absdiff_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a |-| b : N"
+  unfolding arith_defs by typechk
+
+lemma absdiff_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a |-| b = c |-| d : N"
+  unfolding arith_defs by equal
+
+lemma absdiff_self_eq_0: "a:N \<Longrightarrow> a |-| a = 0 : N"
+  unfolding absdiff_def by (arith_rew diff_self_eq_0)
+
+lemma absdiffC0: "a:N \<Longrightarrow> 0 |-| a = a : N"
+  unfolding absdiff_def by hyp_arith_rew
+
+lemma absdiff_succ_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> succ(a) |-| succ(b)  =  a |-| b : N"
+  unfolding absdiff_def by hyp_arith_rew
+
+text \<open>Note how easy using commutative laws can be?  ...not always...\<close>
+lemma absdiff_commute: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a |-| b = b |-| a : N"
+  unfolding absdiff_def
+  apply (rule add_commute)
+   apply (typechk diff_typing)
+  done
+
+text \<open>If \<open>a + b = 0\<close> then \<open>a = 0\<close>. Surprisingly tedious.\<close>
+schematic_goal add_eq0_lemma: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> ?c : Eq(N,a#+b,0) \<longrightarrow> Eq(N,a,0)"
+  apply (NE a)
+    apply (rule_tac [3] replace_type)
+     apply arith_rew
+  apply intr  \<comment> \<open>strips remaining \<open>\<Prod>\<close>s\<close>
+   apply (rule_tac [2] zero_ne_succ [THEN FE])
+     apply (erule_tac [3] EqE [THEN sym_elem])
+    apply (typechk add_typing)
+  done
+
+text \<open>
+  Version of above with the premise \<open>a + b = 0\<close>.
+  Again, resolution instantiates variables in @{thm ProdE}.
+\<close>
+lemma add_eq0: "\<lbrakk>a:N; b:N; a #+ b = 0 : N\<rbrakk> \<Longrightarrow> a = 0 : N"
+  apply (rule EqE)
+  apply (rule add_eq0_lemma [THEN ProdE])
+    apply (rule_tac [3] EqI)
+    apply typechk
+  done
+
+text \<open>Here is a lemma to infer \<open>a - b = 0\<close> and \<open>b - a = 0\<close> from \<open>a |-| b = 0\<close>, below.\<close>
+schematic_goal absdiff_eq0_lem:
+  "\<lbrakk>a:N; b:N; a |-| b = 0 : N\<rbrakk> \<Longrightarrow> ?a : Eq(N, a-b, 0) \<times> Eq(N, b-a, 0)"
+  apply (unfold absdiff_def)
+  apply intr
+   apply eqintr
+   apply (rule_tac [2] add_eq0)
+     apply (rule add_eq0)
+       apply (rule_tac [6] add_commute [THEN trans_elem])
+         apply (typechk diff_typing)
+  done
+
+text \<open>If \<open>a |-| b = 0\<close> then \<open>a = b\<close>
+  proof: \<open>a - b = 0\<close> and \<open>b - a = 0\<close>, so \<open>b = a + (b - a) = a + 0 = a\<close>.
+\<close>
+lemma absdiff_eq0: "\<lbrakk>a |-| b = 0 : N; a:N; b:N\<rbrakk> \<Longrightarrow> a = b : N"
+  apply (rule EqE)
+  apply (rule absdiff_eq0_lem [THEN SumE])
+     apply eqintr
+  apply (rule add_diff_inverse [THEN sym_elem, THEN trans_elem])
+     apply (erule_tac [3] EqE)
+    apply (hyp_arith_rew add_0_right)
+  done
+
+
+subsection \<open>Remainder and Quotient\<close>
+
+text \<open>Typing of remainder: short and long versions.\<close>
+
+lemma mod_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a mod b : N"
+  unfolding mod_def by (typechk absdiff_typing)
+
+lemma mod_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a mod b = c mod d : N"
+  unfolding mod_def by (equal absdiff_typingL)
+
+
+text \<open>Computation for \<open>mod\<close>: 0 and successor cases.\<close>
+
+lemma modC0: "b:N \<Longrightarrow> 0 mod b = 0 : N"
+  unfolding mod_def by (rew absdiff_typing)
+
+lemma modC_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow>
+  succ(a) mod b = rec(succ(a mod b) |-| b, 0, \<lambda>x y. succ(a mod b)) : N"
+  unfolding mod_def by (rew absdiff_typing)
+
+
+text \<open>Typing of quotient: short and long versions.\<close>
+
+lemma div_typing: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a div b : N"
+  unfolding div_def by (typechk absdiff_typing mod_typing)
+
+lemma div_typingL: "\<lbrakk>a = c:N; b = d:N\<rbrakk> \<Longrightarrow> a div b = c div d : N"
+  unfolding div_def by (equal absdiff_typingL mod_typingL)
+
+lemmas div_typing_rls = mod_typing div_typing absdiff_typing
+
+
+text \<open>Computation for quotient: 0 and successor cases.\<close>
+
+lemma divC0: "b:N \<Longrightarrow> 0 div b = 0 : N"
+  unfolding div_def by (rew mod_typing absdiff_typing)
+
+lemma divC_succ: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow>
+  succ(a) div b = rec(succ(a) mod b, succ(a div b), \<lambda>x y. a div b) : N"
+  unfolding div_def by (rew mod_typing)
+
+
+text \<open>Version of above with same condition as the \<open>mod\<close> one.\<close>
+lemma divC_succ2: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow>
+  succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), \<lambda>x y. a div b) : N"
+  apply (rule divC_succ [THEN trans_elem])
+    apply (rew div_typing_rls modC_succ)
+  apply (NE "succ (a mod b) |-|b")
+    apply (rew mod_typing div_typing absdiff_typing)
+  done
+
+text \<open>For case analysis on whether a number is 0 or a successor.\<close>
+lemma iszero_decidable: "a:N \<Longrightarrow> rec(a, inl(eq), \<lambda>ka kb. inr(<ka, eq>)) :
+  Eq(N,a,0) + (\<Sum>x:N. Eq(N,a, succ(x)))"
+  apply (NE a)
+    apply (rule_tac [3] PlusI_inr)
+     apply (rule_tac [2] PlusI_inl)
+      apply eqintr
+     apply equal
+  done
+
+text \<open>Main Result. Holds when \<open>b\<close> is 0 since \<open>a mod 0 = a\<close> and \<open>a div 0 = 0\<close>.\<close>
+lemma mod_div_equality: "\<lbrakk>a:N; b:N\<rbrakk> \<Longrightarrow> a mod b #+ (a div b) #* b = a : N"
+  apply (NE a)
+    apply (arith_rew div_typing_rls modC0 modC_succ divC0 divC_succ2)
+  apply (rule EqE)
+    \<comment> \<open>case analysis on \<open>succ(u mod b) |-| b\<close>\<close>
+  apply (rule_tac a1 = "succ (u mod b) |-| b" in iszero_decidable [THEN PlusE])
+    apply (erule_tac [3] SumE)
+    apply (hyp_arith_rew div_typing_rls modC0 modC_succ divC0 divC_succ2)
+    \<comment> \<open>Replace one occurrence of \<open>b\<close> by \<open>succ(u mod b)\<close>. Clumsy!\<close>
+  apply (rule add_typingL [THEN trans_elem])
+    apply (erule EqE [THEN absdiff_eq0, THEN sym_elem])
+     apply (rule_tac [3] refl_elem)
+     apply (hyp_arith_rew div_typing_rls)
+  done
+
 end
diff -r f556a7a9080c -r f3cd78ba687c src/CTT/Main.thy
--- a/src/CTT/Main.thy	Tue Apr 11 10:29:25 2017 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,6 +0,0 @@
-section \<open>Main includes everything\<close>
-
-theory Main
-  imports CTT Bool Arith
-begin
-end
diff -r f556a7a9080c -r f3cd78ba687c src/CTT/ROOT
--- a/src/CTT/ROOT	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/CTT/ROOT	Wed Apr 12 13:48:07 2017 +0200
@@ -18,7 +18,7 @@
   *}
   options [thy_output_source]
   theories
-    Main
+    CTT
     "ex/Typechecking"
     "ex/Elimination"
     "ex/Equality"
diff -r f556a7a9080c -r f3cd78ba687c src/CTT/ex/Synthesis.thy
--- a/src/CTT/ex/Synthesis.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/CTT/ex/Synthesis.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -6,7 +6,7 @@
 section "Synthesis examples, using a crude form of narrowing"
 
 theory Synthesis
-imports "../Arith"
+imports "../CTT"
 begin
 
 text "discovery of predecessor function"
diff -r f556a7a9080c -r f3cd78ba687c src/Doc/Implementation/Logic.thy
--- a/src/Doc/Implementation/Logic.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Doc/Implementation/Logic.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -70,7 +70,7 @@
   For \<open>k = 1\<close> the parentheses are omitted, e.g.\ \<open>\<alpha> list\<close> instead of
   \<open>(\<alpha>)list\<close>. Further notation is provided for specific constructors, notably
   the right-associative infix \<open>\<alpha> \<Rightarrow> \<beta>\<close> instead of \<open>(\<alpha>, \<beta>)fun\<close>.
-  
+
   The logical category \<^emph>\<open>type\<close> is defined inductively over type variables and
   type constructors as follows: \<open>\<tau> = \<alpha>\<^sub>s | ?\<alpha>\<^sub>s | (\<tau>\<^sub>1, \<dots>, \<tau>\<^sub>k)\<kappa>\<close>.
 
@@ -1186,7 +1186,7 @@
   \begin{mldecls}
   @{index_ML_type proof} \\
   @{index_ML_type proof_body} \\
-  @{index_ML proofs: "int Unsynchronized.ref"} \\
+  @{index_ML Proofterm.proofs: "int Unsynchronized.ref"} \\
   @{index_ML Reconstruct.reconstruct_proof:
   "Proof.context -> term -> proof -> proof"} \\
   @{index_ML Reconstruct.expand_proof: "Proof.context ->
@@ -1215,11 +1215,11 @@
   construction of proofs by introducing dynamic ad-hoc dependencies. Parallel
   performance may suffer by inspecting proof terms at run-time.
 
-  \<^descr> @{ML proofs} specifies the detail of proof recording within @{ML_type thm}
-  values produced by the inference kernel: @{ML 0} records only the names of
-  oracles, @{ML 1} records oracle names and propositions, @{ML 2} additionally
-  records full proof terms. Officially named theorems that contribute to a
-  result are recorded in any case.
+  \<^descr> @{ML Proofterm.proofs} specifies the detail of proof recording within
+  @{ML_type thm} values produced by the inference kernel: @{ML 0} records only
+  the names of oracles, @{ML 1} records oracle names and propositions, @{ML 2}
+  additionally records full proof terms. Officially named theorems that
+  contribute to a result are recorded in any case.
 
   \<^descr> @{ML Reconstruct.reconstruct_proof}~\<open>ctxt prop prf\<close> turns the implicit
   proof term \<open>prf\<close> into a full proof of the given proposition.
diff -r f556a7a9080c -r f3cd78ba687c src/Doc/Logics_ZF/ZF_Isar.thy
--- a/src/Doc/Logics_ZF/ZF_Isar.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Doc/Logics_ZF/ZF_Isar.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -1,5 +1,5 @@
 theory ZF_Isar
-imports Main
+imports ZF
 begin
 
 (*<*)
diff -r f556a7a9080c -r f3cd78ba687c src/Doc/Logics_ZF/ZF_examples.thy
--- a/src/Doc/Logics_ZF/ZF_examples.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Doc/Logics_ZF/ZF_examples.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -1,6 +1,6 @@
 section{*Examples of Reasoning in ZF Set Theory*}
 
-theory ZF_examples imports Main_ZFC begin
+theory ZF_examples imports ZFC begin
 
 subsection {* Binary Trees *}
 
diff -r f556a7a9080c -r f3cd78ba687c src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Apr 12 13:48:07 2017 +0200
@@ -332,7 +332,7 @@
 
 fun thms_of all thy =
   filter
-    (fn th => (all orelse Thm.theory_name_of_thm th = Context.theory_name thy)
+    (fn th => (all orelse Thm.theory_name th = Context.theory_name thy)
       (* andalso is_executable_thm thy th *))
     (map snd (filter_out is_forbidden_theorem (Global_Theory.all_thms_of thy false)))
 
diff -r f556a7a9080c -r f3cd78ba687c src/HOL/Nitpick_Examples/Mono_Nits.thy
--- a/src/HOL/Nitpick_Examples/Mono_Nits.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -153,7 +153,7 @@
 fun theorems_of thy =
   filter (fn (name, th) =>
              not (is_forbidden_theorem name) andalso
-             Thm.theory_name_of_thm th = Context.theory_name thy)
+             Thm.theory_name th = Context.theory_name thy)
          (Global_Theory.all_thms_of thy true)
 
 fun check_formulas tsp =
diff -r f556a7a9080c -r f3cd78ba687c src/HOL/Nunchaku/Tools/nunchaku_collect.ML
--- a/src/HOL/Nunchaku/Tools/nunchaku_collect.ML	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/HOL/Nunchaku/Tools/nunchaku_collect.ML	Wed Apr 12 13:48:07 2017 +0200
@@ -556,7 +556,7 @@
   #> map snd
   #> filter (null o fst)
   #> maps snd
-  #> filter_out (is_builtin_theory o Thm.theory_id_of_thm)
+  #> filter_out (is_builtin_theory o Thm.theory_id)
   #> map Thm.prop_of;
 
 fun keys_of _ (ITVal (T, _)) = [key_of_typ T]
diff -r f556a7a9080c -r f3cd78ba687c src/HOL/Proofs.thy
--- a/src/HOL/Proofs.thy	Tue Apr 11 10:29:25 2017 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,8 +0,0 @@
-theory Proofs
-imports Pure
-begin
-
-ML "Proofterm.proofs := 2"
-
-end
-
diff -r f556a7a9080c -r f3cd78ba687c src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/HOL/ROOT	Wed Apr 12 13:48:07 2017 +0200
@@ -18,8 +18,8 @@
   description {*
     HOL-Main with explicit proof terms.
   *}
-  options [document = false, quick_and_dirty = false, parallel_proofs = 0]
-  theories Proofs (*sequential change of global flag!*)
+  options [document = false, theory_qualifier = "HOL",
+    quick_and_dirty = false, record_proofs = 2, parallel_proofs = 0]
   theories "~~/src/HOL/Library/Old_Datatype"
   files
     "Tools/Quickcheck/Narrowing_Engine.hs"
@@ -60,7 +60,7 @@
 
 session "HOL-Analysis" (main timing) in Analysis = HOL +
   theories
-    Analysis (global)
+    Analysis
   document_files
     "root.tex"
 
@@ -830,7 +830,7 @@
 
 session "HOL-Word" (main timing) in Word = HOL +
   theories
-    Word (global)
+    Word
   document_files "root.bib" "root.tex"
 
 session "HOL-Word-Examples" in "Word/Examples" = "HOL-Word" +
diff -r f556a7a9080c -r f3cd78ba687c src/HOL/TPTP/mash_export.ML
--- a/src/HOL/TPTP/mash_export.ML	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/HOL/TPTP/mash_export.ML	Wed Apr 12 13:48:07 2017 +0200
@@ -58,7 +58,7 @@
   | _ => ("", []))
 
 fun has_thm_thy th thy =
-  Context.theory_name thy = Thm.theory_name_of_thm th
+  Context.theory_name thy = Thm.theory_name th
 
 fun has_thys thys th = exists (has_thm_thy th) thys
 
@@ -98,7 +98,7 @@
     fun do_fact ((_, stature), th) =
       let
         val name = nickname_of_thm th
-        val feats = features_of ctxt (Thm.theory_name_of_thm th) stature [Thm.prop_of th]
+        val feats = features_of ctxt (Thm.theory_name th) stature [Thm.prop_of th]
         val s = encode_str name ^ ": " ^ encode_strs (sort string_ord feats) ^ "\n"
       in
         File.append path s
@@ -188,14 +188,14 @@
           val _ = tracing ("Fact " ^ string_of_int j ^ ": " ^ name)
           val isar_deps = isar_dependencies_of name_tabs th
           val do_query = not (is_bad_query ctxt ho_atp step j th isar_deps)
-          val goal_feats = features_of ctxt (Thm.theory_name_of_thm th) stature [Thm.prop_of th]
+          val goal_feats = features_of ctxt (Thm.theory_name th) stature [Thm.prop_of th]
           val access_facts = filter_accessible_from th new_facts @ old_facts
           val (marker, deps) =
             smart_dependencies_of ctxt params_opt access_facts name_tabs th isar_deps
 
           fun extra_features_of (((_, stature), th), weight) =
             [Thm.prop_of th]
-            |> features_of ctxt (Thm.theory_name_of_thm th) stature
+            |> features_of ctxt (Thm.theory_name th) stature
             |> map (rpair (weight * extra_feature_factor))
 
           val query =
@@ -263,7 +263,7 @@
               val suggs =
                 old_facts
                 |> filter_accessible_from th
-                |> mepo_or_mash_suggested_facts ctxt (Thm.theory_name_of_thm th)
+                |> mepo_or_mash_suggested_facts ctxt (Thm.theory_name th)
                   params max_suggs hyp_ts concl_t
                 |> map (nickname_of_thm o snd)
             in
diff -r f556a7a9080c -r f3cd78ba687c src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Apr 12 13:48:07 2017 +0200
@@ -1360,7 +1360,7 @@
   ctxt |> Spec_Rules.get
        |> filter (curry (op =) Spec_Rules.Unknown o fst)
        |> maps (snd o snd)
-       |> filter_out (is_built_in_theory o Thm.theory_id_of_thm)
+       |> filter_out (is_built_in_theory o Thm.theory_id)
        |> map (subst_atomic subst o Thm.prop_of)
 
 fun arity_of_built_in_const (s, T) =
diff -r f556a7a9080c -r f3cd78ba687c src/HOL/Tools/Quickcheck/find_unused_assms.ML
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Wed Apr 12 13:48:07 2017 +0200
@@ -15,7 +15,7 @@
 
 fun thms_of thy thy_name =
   Global_Theory.all_thms_of thy false
-  |> filter (fn (_, th) => Thm.theory_name_of_thm th = thy_name)
+  |> filter (fn (_, th) => Thm.theory_name th = thy_name)
 
 fun do_while P f s list =
   if P s then
diff -r f556a7a9080c -r f3cd78ba687c src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Wed Apr 12 13:48:07 2017 +0200
@@ -347,7 +347,7 @@
   | normalize_eq t = t
 
 fun if_thm_before th th' =
-  if Context.subthy_id (apply2 Thm.theory_id_of_thm (th, th')) then th else th'
+  if Context.subthy_id (apply2 Thm.theory_id (th, th')) then th else th'
 
 (* Hack: Conflate the facts about a class as seen from the outside with the corresponding low-level
    facts, so that MaSh can learn from the low-level proofs. *)
diff -r f556a7a9080c -r f3cd78ba687c src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Apr 12 13:48:07 2017 +0200
@@ -797,7 +797,7 @@
       (* There must be a better way to detect local facts. *)
       (case Long_Name.dest_local hint of
         SOME suf =>
-        Long_Name.implode [Thm.theory_name_of_thm th, suf, crude_printed_term 25 (Thm.prop_of th)]
+        Long_Name.implode [Thm.theory_name th, suf, crude_printed_term 25 (Thm.prop_of th)]
       | NONE => hint)
     end
   else
@@ -838,7 +838,7 @@
         | _ => string_ord (apply2 Context.theory_id_name p))
   in
     fn p =>
-      (case crude_theory_ord (apply2 Thm.theory_id_of_thm p) of
+      (case crude_theory_ord (apply2 Thm.theory_id p) of
         EQUAL =>
         (* The hack below is necessary because of odd dependencies that are not reflected in the theory
            comparison. *)
@@ -851,7 +851,7 @@
       | ord => ord)
   end;
 
-val thm_less_eq = Context.subthy_id o apply2 Thm.theory_id_of_thm
+val thm_less_eq = Context.subthy_id o apply2 Thm.theory_id
 fun thm_less p = thm_less_eq p andalso not (thm_less_eq (swap p))
 
 val freezeT = Type.legacy_freeze_type
@@ -1124,7 +1124,7 @@
             val chunks = app_hd (cons th) chunks
             val chunks_and_parents' =
               if thm_less_eq (th, th') andalso
-                Thm.theory_name_of_thm th = Thm.theory_name_of_thm th'
+                Thm.theory_name th = Thm.theory_name th'
               then (chunks, [nickname_of_thm th])
               else chunks_and_parents_for chunks th'
           in
@@ -1173,9 +1173,9 @@
   | maximal_wrt_access_graph access_G (fact :: facts) =
     let
       fun cleanup_wrt (_, th) =
-        let val thy_id = Thm.theory_id_of_thm th in
+        let val thy_id = Thm.theory_id th in
           filter_out (fn (_, th') =>
-            Context.proper_subthy_id (Thm.theory_id_of_thm th', thy_id))
+            Context.proper_subthy_id (Thm.theory_id th', thy_id))
         end
 
       fun shuffle_cleanup accum [] = accum
@@ -1229,11 +1229,11 @@
 
     val chained = filter (fn ((_, (scope, _)), _) => scope = Chained) facts
 
-    fun fact_has_right_theory (_, th) = thy_name = Thm.theory_name_of_thm th
+    fun fact_has_right_theory (_, th) = thy_name = Thm.theory_name th
 
     fun chained_or_extra_features_of factor (((_, stature), th), weight) =
       [Thm.prop_of th]
-      |> features_of ctxt (Thm.theory_name_of_thm th) stature
+      |> features_of ctxt (Thm.theory_name th) stature
       |> map (rpair (weight * factor))
   in
     (case get_state ctxt of
@@ -1454,7 +1454,7 @@
                   (learns, (num_nontrivial, next_commit, _)) =
                 let
                   val name = nickname_of_thm th
-                  val feats = features_of ctxt (Thm.theory_name_of_thm th) stature [Thm.prop_of th]
+                  val feats = features_of ctxt (Thm.theory_name th) stature [Thm.prop_of th]
                   val deps = these (deps_of status th)
                   val num_nontrivial = num_nontrivial |> not (null deps) ? Integer.add 1
                   val learns = (name, parents, feats, deps) :: learns
diff -r f556a7a9080c -r f3cd78ba687c src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mepo.ML	Wed Apr 12 13:48:07 2017 +0200
@@ -220,7 +220,7 @@
     t
 
 fun theory_const_prop_of fudge th =
-  theory_constify fudge (Thm.theory_name_of_thm th) (Thm.prop_of th)
+  theory_constify fudge (Thm.theory_name th) (Thm.prop_of th)
 
 fun pair_consts_fact thy fudge fact =
   (case fact |> snd |> theory_const_prop_of fudge |> pconsts_in_fact thy of
diff -r f556a7a9080c -r f3cd78ba687c src/Pure/General/long_name.scala
--- a/src/Pure/General/long_name.scala	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Pure/General/long_name.scala	Wed Apr 12 13:48:07 2017 +0200
@@ -21,6 +21,10 @@
     if (qual == "" || name == "") name
     else qual + separator + name
 
+  def qualifier(name: String): String =
+    if (name == "") ""
+    else implode(explode(name).dropRight(1))
+
   def base_name(name: String): String =
     if (name == "") ""
     else explode(name).last
diff -r f556a7a9080c -r f3cd78ba687c src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Pure/Isar/proof.ML	Wed Apr 12 13:48:07 2017 +0200
@@ -515,7 +515,7 @@
     val thy = Proof_Context.theory_of ctxt;
 
     val _ =
-      Context.subthy_id (Thm.theory_id_of_thm goal, Context.theory_id thy) orelse
+      Context.subthy_id (Thm.theory_id goal, Context.theory_id thy) orelse
         error "Bad background theory of goal state";
     val _ = Thm.no_prems goal orelse error (Proof_Display.string_of_goal ctxt goal);
 
diff -r f556a7a9080c -r f3cd78ba687c src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Pure/PIDE/document.ML	Wed Apr 12 13:48:07 2017 +0200
@@ -177,9 +177,6 @@
     SOME eval => Command.eval_finished eval
   | NONE => false);
 
-fun loaded_theory name =
-  get_first Thy_Info.lookup_theory [name, Long_Name.base_name name];
-
 fun get_node nodes name = String_Graph.get_node nodes name
   handle String_Graph.UNDEF _ => empty_node;
 fun default_node name = String_Graph.default_node (name, empty_node);
@@ -463,7 +460,7 @@
       val delay_request' = Event_Timer.future (Time.now () + delay);
 
       fun finished_import (name, (node, _)) =
-        finished_result node orelse is_some (loaded_theory name);
+        finished_result node orelse is_some (Thy_Info.lookup_theory name);
 
       val nodes = nodes_of (the_version state version_id);
       val required = make_required nodes;
@@ -530,7 +527,7 @@
         handle ERROR msg => (Output.error_message msg; NONE);
     val parents_reports =
       imports |> map_filter (fn (import, pos) =>
-        (case loaded_theory import of
+        (case Thy_Info.lookup_theory import of
           NONE =>
             maybe_end_theory pos
               (case get_result (snd (the (AList.lookup (op =) deps import))) of
@@ -554,7 +551,7 @@
   else NONE;
 
 fun check_theory full name node =
-  is_some (loaded_theory name) orelse
+  is_some (Thy_Info.lookup_theory name) orelse
   null (#errors (get_header node)) andalso (not full orelse is_some (get_result node));
 
 fun last_common keywords state node_required node0 node =
diff -r f556a7a9080c -r f3cd78ba687c src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Apr 12 13:48:07 2017 +0200
@@ -117,6 +117,8 @@
       def loaded_theory: Name = Name(theory, "", theory)
       def is_theory: Boolean = theory.nonEmpty
 
+      def theory_base_name: String = Long_Name.base_name(theory)
+
       override def toString: String = if (is_theory) theory else node
 
       def map(f: String => String): Name = copy(f(node), f(master_dir), theory)
diff -r f556a7a9080c -r f3cd78ba687c src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Pure/PIDE/protocol.scala	Wed Apr 12 13:48:07 2017 +0200
@@ -359,14 +359,13 @@
           { case Document.Node.Edits(a) => (Nil, list(pair(option(id), option(id)))(a)) },
           { case Document.Node.Deps(header) =>
               val master_dir = File.standard_url(name.master_dir)
-              val theory = Long_Name.base_name(name.theory)
               val imports = header.imports.map({ case (a, _) => a.node })
               val keywords =
                 header.keywords.map({ case (a, Keyword.Spec(b, c, d)) => (a, ((b, c), d)) })
               (Nil,
                 pair(string, pair(string, pair(list(string), pair(list(pair(string,
                     pair(pair(string, list(string)), list(string)))), list(string)))))(
-                (master_dir, (theory, (imports, (keywords, header.errors)))))) },
+                (master_dir, (name.theory, (imports, (keywords, header.errors)))))) },
           { case Document.Node.Perspective(a, b, c) =>
               (bool_atom(a) :: b.commands.map(cmd => long_atom(cmd.id)),
                 list(pair(id, pair(string, list(string))))(c.dest)) }))
diff -r f556a7a9080c -r f3cd78ba687c src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Pure/PIDE/resources.ML	Wed Apr 12 13:48:07 2017 +0200
@@ -6,12 +6,22 @@
 
 signature RESOURCES =
 sig
-  val set_session_base: {known_theories: (string * string) list} -> unit
+  val set_session_base:
+    {default_qualifier: string,
+     global_theories: (string * string) list,
+     loaded_theories: (string * string) list,
+     known_theories: (string * string) list} -> unit
   val reset_session_base: unit -> unit
+  val default_qualifier: unit -> string
+  val global_theory: string -> string option
+  val loaded_theory: string -> Path.T option
   val known_theory: string -> Path.T option
   val master_directory: theory -> Path.T
   val imports_of: theory -> (string * Position.T) list
   val thy_path: Path.T -> Path.T
+  val theory_qualifier: string -> string
+  val import_name: string -> Path.T -> string ->
+    {node_name: Path.T, master_dir: Path.T, theory_name: string}
   val check_thy: Path.T -> string ->
    {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
     imports: (string * Position.T) list, keywords: Thy_Header.keywords}
@@ -30,19 +40,34 @@
 
 (* session base *)
 
+val init_session_base =
+  {default_qualifier = "Draft",
+   global_theories = Symtab.empty: string Symtab.table,
+   loaded_theories = Symtab.empty: Path.T Symtab.table,
+   known_theories = Symtab.empty: Path.T Symtab.table};
+
 val global_session_base =
-  Synchronized.var "Sessions.base"
-    ({known_theories = Symtab.empty: Path.T Symtab.table});
+  Synchronized.var "Sessions.base" init_session_base;
 
-fun set_session_base {known_theories} =
+fun set_session_base {default_qualifier, global_theories, loaded_theories, known_theories} =
   Synchronized.change global_session_base
-    (K {known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
+    (fn _ =>
+      {default_qualifier =
+        if default_qualifier <> "" then default_qualifier
+        else #default_qualifier init_session_base,
+       global_theories = Symtab.make global_theories,
+       loaded_theories = Symtab.make (map (apsnd Path.explode) loaded_theories),
+       known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
 
 fun reset_session_base () =
-  set_session_base {known_theories = []};
+  Synchronized.change global_session_base (K init_session_base);
+
+fun get_session_base f = f (Synchronized.value global_session_base);
 
-fun known_theory name =
-  Symtab.lookup (#known_theories (Synchronized.value global_session_base)) name;
+fun default_qualifier () = get_session_base #default_qualifier;
+fun global_theory a = Symtab.lookup (get_session_base #global_theories) a;
+fun loaded_theory a = Symtab.lookup (get_session_base #loaded_theories) a;
+fun known_theory a = Symtab.lookup (get_session_base #known_theories) a;
 
 
 (* manage source files *)
@@ -78,16 +103,36 @@
 
 val thy_path = Path.ext "thy";
 
+fun theory_qualifier theory =
+  (case global_theory theory of
+    SOME qualifier => qualifier
+  | NONE => Long_Name.qualifier theory);
+
+fun import_name qualifier dir s =
+  let
+    val theory0 = Thy_Header.import_name s;
+    val theory =
+      if Long_Name.is_qualified theory0 orelse is_some (global_theory theory0)
+        orelse true (* FIXME *) then theory0
+      else Long_Name.qualify qualifier theory0;
+    val node_name =
+      the (get_first (fn e => e ())
+        [fn () => loaded_theory theory,
+         fn () => loaded_theory theory0,
+         fn () => known_theory theory,
+         fn () => known_theory theory0,
+         fn () => SOME (File.full_path dir (thy_path (Path.expand (Path.explode s))))])
+  in {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory} end;
+
 fun check_file dir file = File.check_file (File.full_path dir file);
 
 fun check_thy dir thy_name =
   let
     val thy_base_name = Long_Name.base_name thy_name;
-    val thy_path = thy_path (Path.basic thy_base_name);
     val master_file =
       (case known_theory thy_name of
-        NONE => check_file dir thy_path
-      | SOME known_path => check_file Path.current known_path);
+        SOME known_path => check_file Path.current known_path
+      | NONE => check_file dir (thy_path (Path.basic thy_base_name)));
     val text = File.read master_file;
 
     val {name = (name, pos), imports, keywords} =
@@ -95,7 +140,7 @@
     val _ =
       thy_base_name <> name andalso
         error ("Bad theory name " ^ quote name ^
-          " for file " ^ Path.print thy_path ^ Position.here pos);
+          " for file " ^ Path.print (Path.base master_file) ^ Position.here pos);
   in
    {master = (master_file, SHA1.digest text), text = text, theory_pos = pos,
     imports = imports, keywords = keywords}
diff -r f556a7a9080c -r f3cd78ba687c src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Wed Apr 12 13:48:07 2017 +0200
@@ -14,8 +14,8 @@
 
 
 class Resources(
-  val session_name: String,
   val session_base: Sessions.Base,
+  val default_qualifier: String = Sessions.DRAFT,
   val log: Logger = No_Logger)
 {
   val thy_info = new Thy_Info(this)
@@ -67,12 +67,16 @@
     }
     else Nil
 
-  def import_name(dir: String, s: String): Document.Node.Name =
+  def theory_qualifier(name: Document.Node.Name): String =
+    session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
+
+  def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
   {
-    val theory0 = Thy_Header.base_name(s)
+    val theory0 = Thy_Header.import_name(s)
     val theory =
-      if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0)) theory0
-      else Long_Name.qualify(session_name, theory0)
+      if (Long_Name.is_qualified(theory0) || session_base.global_theories.isDefinedAt(theory0)
+        || true /* FIXME */) theory0
+      else theory0 // FIXME Long_Name.qualify(qualifier, theory0)
 
     session_base.loaded_theories.get(theory) orElse
     session_base.loaded_theories.get(theory0) orElse
@@ -101,7 +105,7 @@
       try {
         val header = Thy_Header.read(reader, start, strict).decode_symbols
 
-        val base_name = Long_Name.base_name(node_name.theory)
+        val base_name = node_name.theory_base_name
         val (name, pos) = header.name
         if (base_name != name)
           error("Bad theory name " + quote(name) +
@@ -109,7 +113,8 @@
             Completion.report_names(pos, 1, List((base_name, ("theory", base_name)))))
 
         val imports =
-          header.imports.map({ case (s, pos) => (import_name(node_name.master_dir, s), pos) })
+          header.imports.map({ case (s, pos) =>
+            (import_name(theory_qualifier(node_name), node_name.master_dir, s), pos) })
         Document.Node.Header(imports, header.keywords, header.abbrevs)
       }
       catch { case exn: Throwable => Document.Node.bad_header(Exn.message(exn)) }
@@ -125,13 +130,20 @@
   /* special header */
 
   def special_header(name: Document.Node.Name): Option[Document.Node.Header] =
-    if (Thy_Header.is_ml_root(name.theory))
-      Some(Document.Node.Header(
-        List((import_name(name.master_dir, Thy_Header.ML_BOOTSTRAP), Position.none))))
-    else if (Thy_Header.is_bootstrap(name.theory))
-      Some(Document.Node.Header(
-        List((import_name(name.master_dir, Thy_Header.PURE), Position.none))))
-    else None
+  {
+    val qualifier = theory_qualifier(name)
+    val dir = name.master_dir
+
+    val imports =
+      if (Thy_Header.is_ml_root(name.theory))
+        List(import_name(qualifier, dir, Thy_Header.ML_BOOTSTRAP))
+      else if (Thy_Header.is_bootstrap(name.theory))
+        List(import_name(qualifier, dir, Thy_Header.PURE))
+      else Nil
+
+    if (imports.isEmpty) None
+    else Some(Document.Node.Header(imports.map((_, Position.none))))
+  }
 
 
   /* blobs */
diff -r f556a7a9080c -r f3cd78ba687c src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Pure/System/isabelle_process.ML	Wed Apr 12 13:48:07 2017 +0200
@@ -219,6 +219,8 @@
   Multithreading.trace := Options.default_int "threads_trace";
   Multithreading.max_threads_update (Options.default_int "threads");
   Goal.parallel_proofs := Options.default_int "parallel_proofs";
+  let val proofs = Options.default_int "record_proofs"
+  in if proofs < 0 then () else Proofterm.proofs := proofs end;
   Printer.show_markup_default := false);
 
 fun init_options_interactive () =
diff -r f556a7a9080c -r f3cd78ba687c src/Pure/System/isabelle_tool.scala
--- a/src/Pure/System/isabelle_tool.scala	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Pure/System/isabelle_tool.scala	Wed Apr 12 13:48:07 2017 +0200
@@ -57,7 +57,7 @@
 
   private def is_external(dir: Path, file_name: String): Boolean =
   {
-    val file = (dir + Path.basic(file_name)).file
+    val file = (dir + Path.explode(file_name)).file
     try {
       file.isFile && file.canRead &&
         (file_name.endsWith(".scala") || file.canExecute) &&
@@ -73,7 +73,7 @@
       dir <- dirs() if dir.is_dir
       file_name <- File.read_dir(dir) if is_external(dir, file_name)
     } yield {
-      val source = File.read(dir + Path.basic(file_name))
+      val source = File.read(dir + Path.explode(file_name))
       val name = Library.try_unsuffix(".scala", file_name) getOrElse file_name
       val description =
         split_lines(source).collectFirst({ case Description(s) => s }) getOrElse ""
@@ -84,11 +84,11 @@
   private def find_external(name: String): Option[List[String] => Unit] =
     dirs.collectFirst({
       case dir if is_external(dir, name + ".scala") =>
-        compile(dir + Path.basic(name + ".scala"))
+        compile(dir + Path.explode(name + ".scala"))
       case dir if is_external(dir, name) =>
         (args: List[String]) =>
           {
-            val tool = dir + Path.basic(name)
+            val tool = dir + Path.explode(name)
             val result = Isabelle_System.bash(File.bash_path(tool) + " " + Bash.strings(args))
             sys.exit(result.print_stdout.rc)
           }
diff -r f556a7a9080c -r f3cd78ba687c src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Pure/Thy/present.ML	Wed Apr 12 13:48:07 2017 +0200
@@ -67,7 +67,7 @@
         val name = Context.theory_name thy;
         val deps = map (node_name o Context.theory_name) (Theory.parents_of thy);
       in
-        if parent_loaded name then NONE
+        if parent_loaded (Context.theory_long_name thy) then NONE
         else SOME ((node_name name, Graph_Display.content_node name []), deps)
       end;
   in
diff -r f556a7a9080c -r f3cd78ba687c src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed Apr 12 13:48:07 2017 +0200
@@ -6,6 +6,7 @@
 
 package isabelle
 
+import java.io.{File => JFile}
 import java.nio.ByteBuffer
 import java.nio.channels.FileChannel
 import java.nio.file.StandardOpenOption
@@ -19,8 +20,15 @@
 {
   /* base info and source dependencies */
 
+  val DRAFT = "Draft"
+
   def is_pure(name: String): Boolean = name == Thy_Header.PURE
 
+  sealed case class Known_Theories(
+    known_theories: Map[String, Document.Node.Name] = Map.empty,
+    known_theories_local: Map[String, Document.Node.Name] = Map.empty,
+    known_files: Map[JFile, List[Document.Node.Name]] = Map.empty)
+
   object Base
   {
     def pure(options: Options): Base = session_base(options, Thy_Header.PURE)
@@ -28,49 +36,94 @@
     lazy val bootstrap: Base =
       Base(keywords = Thy_Header.bootstrap_header, syntax = Thy_Header.bootstrap_syntax)
 
-    private[Sessions] def known_theories(bases: Iterable[Base], names: Iterable[Document.Node.Name])
-      : Map[String, Document.Node.Name] =
+    private[Sessions] def known_theories(
+        local_dir: Path,
+        bases: List[Base],
+        theories: List[Document.Node.Name]): Known_Theories =
     {
-      val bases_iterator =
-        for { base <- bases.iterator; (_, name) <- base.known_theories.iterator }
-          yield name
+      def bases_iterator(local: Boolean) =
+        for {
+          base <- bases.iterator
+          (_, name) <- (if (local) base.known_theories_local else base.known_theories).iterator
+        } yield name
+
+      def local_theories_iterator =
+      {
+        val local_path = local_dir.file.getCanonicalFile.toPath
+        theories.iterator.filter(name =>
+          Path.explode(name.node).file.getCanonicalFile.toPath.startsWith(local_path))
+      }
 
-      (Map.empty[String, Document.Node.Name] /: (bases_iterator ++ names.iterator))({
-        case (known, name) =>
-          known.get(name.theory) match {
-            case Some(name1) if name != name1 =>
-              error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node))
-            case _ => known + (name.theory -> name)
-          }
+      val known_theories =
+        (Map.empty[String, Document.Node.Name] /: (bases_iterator(false) ++ theories.iterator))({
+          case (known, name) =>
+            known.get(name.theory) match {
+              case Some(name1) if name != name1 =>
+                error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node))
+              case _ => known + (name.theory -> name)
+            }
+          })
+      val known_theories_local =
+        (Map.empty[String, Document.Node.Name] /:
+            (bases_iterator(true) ++ local_theories_iterator))({
+          case (known, name) => known + (name.theory -> name)
         })
+      val known_files =
+        (Map.empty[JFile, List[Document.Node.Name]] /:
+            (bases_iterator(true) ++ bases_iterator(false) ++ theories.iterator))({
+          case (known, name) =>
+            val file = Path.explode(name.node).file.getCanonicalFile
+            val theories1 = known.getOrElse(file, Nil)
+            if (theories1.exists(name1 => name.node == name1.node && name.theory == name1.theory))
+              known
+            else known + (file -> (name :: theories1))
+        })
+      Known_Theories(known_theories, known_theories_local,
+        known_files.iterator.map(p => (p._1, p._2.reverse)).toMap)
     }
   }
 
   sealed case class Base(
-    global_theories: Set[String] = Set.empty,
+    global_theories: Map[String, String] = Map.empty,
     loaded_theories: Map[String, Document.Node.Name] = Map.empty,
     known_theories: Map[String, Document.Node.Name] = Map.empty,
+    known_theories_local: Map[String, Document.Node.Name] = Map.empty,
+    known_files: Map[JFile, List[Document.Node.Name]] = Map.empty,
     keywords: Thy_Header.Keywords = Nil,
     syntax: Outer_Syntax = Outer_Syntax.empty,
     sources: List[(Path, SHA1.Digest)] = Nil,
     session_graph: Graph_Display.Graph = Graph_Display.empty_graph)
   {
+    def platform_path: Base =
+      copy(
+        loaded_theories =
+          for ((a, b) <- loaded_theories) yield (a, b.map(File.platform_path(_))),
+        known_theories =
+          for ((a, b) <- known_theories) yield (a, b.map(File.platform_path(_))),
+        known_theories_local =
+          for ((a, b) <- known_theories_local) yield (a, b.map(File.platform_path(_))),
+        known_files =
+          for ((a, b) <- known_files) yield (a, b.map(c => c.map(File.platform_path(_)))))
+
     def loaded_theory(name: Document.Node.Name): Boolean =
       loaded_theories.isDefinedAt(name.theory)
 
+    def dest_loaded_theories: List[(String, String)] =
+      for ((theory, node_name) <- loaded_theories.toList)
+        yield (theory, node_name.node)
+
     def dest_known_theories: List[(String, String)] =
       for ((theory, node_name) <- known_theories.toList)
         yield (theory, node_name.node)
   }
 
-  sealed case class Deps(sessions: Map[String, Base])
+  sealed case class Deps(
+    session_bases: Map[String, Base],
+    all_known_theories: Known_Theories)
   {
-    def is_empty: Boolean = sessions.isEmpty
-    def apply(name: String): Base = sessions(name)
-    def sources(name: String): List[SHA1.Digest] = sessions(name).sources.map(_._2)
-
-    def all_known_theories: Map[String, Document.Node.Name] =
-      Base.known_theories(sessions.toList.map(_._2), Nil)
+    def is_empty: Boolean = session_bases.isEmpty
+    def apply(name: String): Base = session_bases(name)
+    def sources(name: String): List[SHA1.Digest] = session_bases(name).sources.map(_._2)
   }
 
   def deps(sessions: T,
@@ -79,89 +132,105 @@
       verbose: Boolean = false,
       list_files: Boolean = false,
       check_keywords: Set[String] = Set.empty,
-      global_theories: Set[String] = Set.empty): Deps =
+      global_theories: Map[String, String] = Map.empty,
+      all_known_theories: Boolean = false): Deps =
   {
-    Deps((Map.empty[String, Base] /: sessions.imports_topological_order)({
-      case (sessions, (session_name, info)) =>
-        if (progress.stopped) throw Exn.Interrupt()
+    val session_bases =
+      (Map.empty[String, Base] /: sessions.imports_topological_order)({
+        case (session_bases, (session_name, info)) =>
+          if (progress.stopped) throw Exn.Interrupt()
 
-        try {
-          val parent_base =
-            info.parent match {
-              case None => Base.bootstrap
-              case Some(parent) => sessions(parent)
-            }
-          val resources = new Resources(session_name, parent_base)
+          try {
+            val parent_base =
+              info.parent match {
+                case None => Base.bootstrap
+                case Some(parent) => session_bases(parent)
+              }
+            val resources = new Resources(parent_base,
+              default_qualifier = info.theory_qualifier(session_name))
 
-          if (verbose || list_files) {
-            val groups =
-              if (info.groups.isEmpty) ""
-              else info.groups.mkString(" (", " ", ")")
-            progress.echo("Session " + info.chapter + "/" + session_name + groups)
-          }
+            if (verbose || list_files) {
+              val groups =
+                if (info.groups.isEmpty) ""
+                else info.groups.mkString(" (", " ", ")")
+              progress.echo("Session " + info.chapter + "/" + session_name + groups)
+            }
 
-          val thy_deps =
-          {
-            val root_theories =
-              info.theories.flatMap({ case (_, thys) =>
-                thys.map(thy => (resources.import_name(info.dir.implode, thy), info.pos))
-              })
-            val thy_deps = resources.thy_info.dependencies(root_theories)
+            val thy_deps =
+            {
+              val root_theories =
+                info.theories.flatMap({ case (_, thys) =>
+                  thys.map(thy =>
+                    (resources.import_name(session_name, info.dir.implode, thy), info.pos))
+                })
+              val thy_deps = resources.thy_info.dependencies(root_theories)
 
-            thy_deps.errors match {
-              case Nil => thy_deps
-              case errs => error(cat_lines(errs))
+              thy_deps.errors match {
+                case Nil => thy_deps
+                case errs => error(cat_lines(errs))
+              }
             }
-          }
 
-          val syntax = thy_deps.syntax
+            val known_theories =
+              Base.known_theories(info.dir,
+                parent_base :: info.imports.map(session_bases(_)),
+                thy_deps.deps.map(_.name))
+
+            val syntax = thy_deps.syntax
 
-          val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
-          val loaded_files =
-            if (inlined_files) {
-              val pure_files =
-                if (is_pure(session_name)) {
-                  val roots = Thy_Header.ml_roots.map(p => info.dir + Path.explode(p._1))
-                  val files =
-                    roots.flatMap(root => resources.loaded_files(syntax, File.read(root))).
-                      map(file => info.dir + Path.explode(file))
-                  roots ::: files
-                }
-                else Nil
-              pure_files ::: thy_deps.loaded_files
-            }
-            else Nil
+            val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
+            val loaded_files =
+              if (inlined_files) {
+                val pure_files =
+                  if (is_pure(session_name)) {
+                    val roots = Thy_Header.ml_roots.map(p => info.dir + Path.explode(p._1))
+                    val files =
+                      roots.flatMap(root => resources.loaded_files(syntax, File.read(root))).
+                        map(file => info.dir + Path.explode(file))
+                    roots ::: files
+                  }
+                  else Nil
+                pure_files ::: thy_deps.loaded_files
+              }
+              else Nil
 
-          val all_files =
-            (theory_files ::: loaded_files :::
-              info.files.map(file => info.dir + file) :::
-              info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
+            val all_files =
+              (theory_files ::: loaded_files :::
+                info.files.map(file => info.dir + file) :::
+                info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
+
+            if (list_files)
+              progress.echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
+
+            if (check_keywords.nonEmpty)
+              Check_Keywords.check_keywords(progress, syntax.keywords, check_keywords, theory_files)
 
-          if (list_files)
-            progress.echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
-
-          if (check_keywords.nonEmpty)
-            Check_Keywords.check_keywords(progress, syntax.keywords, check_keywords, theory_files)
+            val base =
+              Base(global_theories = global_theories,
+                loaded_theories = thy_deps.loaded_theories,
+                known_theories = known_theories.known_theories,
+                known_theories_local = known_theories.known_theories_local,
+                known_files = known_theories.known_files,
+                keywords = thy_deps.keywords,
+                syntax = syntax,
+                sources = all_files.map(p => (p, SHA1.digest(p.file))),
+                session_graph = thy_deps.session_graph(info.parent getOrElse "", parent_base))
 
-          val base =
-            Base(global_theories = global_theories,
-              loaded_theories = thy_deps.loaded_theories,
-              known_theories =
-                Base.known_theories(
-                  parent_base :: info.imports.map(sessions(_)), thy_deps.deps.map(_.name)),
-              keywords = thy_deps.keywords,
-              syntax = syntax,
-              sources = all_files.map(p => (p, SHA1.digest(p.file))),
-              session_graph = thy_deps.session_graph(info.parent getOrElse "", parent_base))
+            session_bases + (session_name -> base)
+          }
+          catch {
+            case ERROR(msg) =>
+              cat_error(msg, "The error(s) above occurred in session " +
+                quote(session_name) + Position.here(info.pos))
+          }
+      })
 
-          sessions + (session_name -> base)
-        }
-        catch {
-          case ERROR(msg) =>
-            cat_error(msg, "The error(s) above occurred in session " +
-              quote(session_name) + Position.here(info.pos))
-        }
-    }))
+    val known_theories =
+      if (all_known_theories)
+        Base.known_theories(Path.current, session_bases.toList.map(_._2), Nil)
+      else Known_Theories()
+
+    Deps(session_bases, known_theories)
   }
 
   def session_base(
@@ -175,8 +244,12 @@
     val selected_sessions = full_sessions.selection(Selection(sessions = List(session)))._2
 
     if (all_known_theories) {
-      val deps = Sessions.deps(full_sessions, global_theories = global_theories)
-      deps(session).copy(known_theories = deps.all_known_theories)
+      val deps = Sessions.deps(
+        full_sessions, global_theories = global_theories, all_known_theories = all_known_theories)
+      deps(session).copy(
+        known_theories = deps.all_known_theories.known_theories,
+        known_theories_local = deps.all_known_theories.known_theories_local,
+        known_files = deps.all_known_theories.known_files)
     }
     else
       deps(selected_sessions, global_theories = global_theories)(session)
@@ -202,6 +275,12 @@
     meta_digest: SHA1.Digest)
   {
     def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
+
+    def theory_qualifier(default_qualifier: String): String =
+      options.string("theory_qualifier") match {
+        case "" => default_qualifier
+        case qualifier => qualifier
+      }
   }
 
   object Selection
@@ -310,17 +389,19 @@
     def get(name: String): Option[Info] =
       if (imports_graph.defined(name)) Some(imports_graph.get_node(name)) else None
 
-    def global_theories: Set[String] =
-      (Set.empty[String] /:
+    def global_theories: Map[String, String] =
+      (Map.empty[String, String] /:
         (for {
-          (_, (info, _)) <- imports_graph.iterator
-          thy <- info.global_theories.iterator }
-         yield (thy, info.pos)))(
-          { case (set, (thy, pos)) =>
-             if (set.contains(thy))
-               error("Duplicate declaration of global theory " + quote(thy) + Position.here(pos))
-             else set + thy
-           })
+          (session_name, (info, _)) <- imports_graph.iterator
+          thy <- info.global_theories.iterator } yield (thy, session_name, info)))({
+            case (global, (thy, session_name, info)) =>
+              val qualifier = info.theory_qualifier(session_name)
+              global.get(thy) match {
+                case Some(qualifier1) if qualifier != qualifier1 =>
+                  error("Duplicate global theory " + quote(thy) + Position.here(info.pos))
+                case _ => global + (thy -> qualifier)
+              }
+          })
 
     def selection(select: Selection): (List[String], T) =
     {
@@ -446,7 +527,7 @@
         try {
           val name = entry.name
 
-          if (name == "") error("Bad session name")
+          if (name == "" || name == DRAFT) error("Bad session name")
           if (is_pure(name) && entry.parent.isDefined) error("Illegal parent session")
           if (!is_pure(name) && !entry.parent.isDefined) error("Missing parent session")
 
diff -r f556a7a9080c -r f3cd78ba687c src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Pure/Thy/thy_header.ML	Wed Apr 12 13:48:07 2017 +0200
@@ -20,6 +20,7 @@
   val ml_bootstrapN: string
   val ml_roots: string list
   val bootstrap_thys: string list
+  val import_name: string -> string
   val args: header parser
   val read: Position.T -> string -> header
   val read_tokens: Token.T list -> header
@@ -113,6 +114,7 @@
 val ml_roots = ["ML_Root0", "ML_Root"];
 val bootstrap_thys = ["Bootstrap_Pure", "Bootstrap_ML_Bootstrap"];
 
+val import_name = Path.implode o Path.base o Path.explode;
 
 
 (* header args *)
diff -r f556a7a9080c -r f3cd78ba687c src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Pure/Thy/thy_header.scala	Wed Apr 12 13:48:07 2017 +0200
@@ -77,21 +77,19 @@
   val ml_roots = List("ROOT0.ML" -> "ML_Root0", "ROOT.ML" -> ML_ROOT)
   val bootstrap_thys = List(PURE, ML_BOOTSTRAP).map(a => a -> ("Bootstrap_" + a))
 
-  private val Base_Name = new Regex(""".*?([^/\\:]+)""")
-  private val Thy_Name = new Regex(""".*?([^/\\:]+)\.thy""")
+  private val Thy_File_Name = new Regex(""".*?([^/\\:]+)\.thy""")
+  private val Import_Name = new Regex(""".*?([^/\\:]+)""")
 
-  def base_name(s: String): String =
-    s match { case Base_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
+  def import_name(s: String): String =
+    s match { case Import_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
 
-  def thy_name(s: String): Option[String] =
-    s match { case Thy_Name(name) => Some(name) case _ => None }
-
-  def thy_name_bootstrap(s: String): Option[String] =
+  def theory_name(s: String): String =
     s match {
-      case Thy_Name(name) =>
-        Some(bootstrap_thys.collectFirst({ case (a, b) if a == name => b }).getOrElse(name))
-      case Base_Name(name) => ml_roots.collectFirst({ case (a, b) if a == name => b })
-      case _ => None
+      case Thy_File_Name(name) =>
+        bootstrap_thys.collectFirst({ case (a, b) if a == name => b }).getOrElse(name)
+      case Import_Name(name) =>
+        ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("")
+      case _ => ""
     }
 
   def is_ml_root(theory: String): Boolean =
diff -r f556a7a9080c -r f3cd78ba687c src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed Apr 12 13:48:07 2017 +0200
@@ -17,9 +17,9 @@
     {document: bool,
      symbols: HTML.symbols,
      last_timing: Toplevel.transition -> Time.time,
+     qualifier: string,
      master_dir: Path.T} -> (string * Position.T) list -> unit
-  val use_thys: (string * Position.T) list -> unit
-  val use_thy: string * Position.T -> unit
+  val use_thy: string -> unit
   val script_thy: Position.T -> string -> theory -> theory
   val register_thy: theory -> unit
   val finish: unit -> unit
@@ -54,11 +54,9 @@
 
 fun make_deps master imports : deps = {master = master, imports = imports};
 
-fun master_dir (d: deps option) =
+fun master_dir_deps (d: deps option) =
   the_default Path.current (Option.map (Path.dir o #1 o #master) d);
 
-fun base_name s = Path.implode (Path.base (Path.explode s));
-
 local
   val global_thys =
     Synchronized.var "Thy_Info.thys"
@@ -88,7 +86,7 @@
 
 val lookup_deps = Option.map #1 o lookup_thy;
 
-val master_directory = master_dir o #1 o get_thy;
+val master_directory = master_dir_deps o #1 o get_thy;
 
 
 (* access theory *)
@@ -130,8 +128,8 @@
 
 fun update deps theory thys =
   let
-    val name = Context.theory_name theory;
-    val parents = map Context.theory_name (Theory.parents_of theory);
+    val name = Context.theory_long_name theory;
+    val parents = map Context.theory_long_name (Theory.parents_of theory);
 
     val thys' = remove name thys;
     val _ = map (get thys') parents;
@@ -286,44 +284,45 @@
 
 in
 
-fun require_thys document symbols last_timing initiators dir strs tasks =
-      fold_map (require_thy document symbols last_timing initiators dir) strs tasks |>> forall I
-and require_thy document symbols last_timing initiators dir (str, require_pos) tasks =
+fun require_thys document symbols last_timing initiators qualifier dir strs tasks =
+      fold_map (require_thy document symbols last_timing initiators qualifier dir) strs tasks
+      |>> forall I
+and require_thy document symbols last_timing initiators qualifier dir (s, require_pos) tasks =
   let
-    val path = Path.expand (Path.explode str);
-    val name = Path.implode (Path.base path);
-    val node_name = File.full_path dir (Resources.thy_path path);
+    val {node_name, master_dir, theory_name} = Resources.import_name qualifier dir s;
     fun check_entry (Task (node_name', _, _)) =
           if op = (apply2 File.platform_path (node_name, node_name'))
           then ()
           else
-            error ("Incoherent imports for theory " ^ quote name ^
+            error ("Incoherent imports for theory " ^ quote theory_name ^
               Position.here require_pos ^ ":\n" ^
               "  " ^ Path.print node_name ^ "\n" ^
               "  " ^ Path.print node_name')
       | check_entry _ = ();
   in
-    (case try (String_Graph.get_node tasks) name of
+    (case try (String_Graph.get_node tasks) theory_name of
       SOME task => (check_entry task; (task_finished task, tasks))
     | NONE =>
         let
-          val dir' = Path.append dir (Path.dir path);
-          val _ = member (op =) initiators name andalso error (cycle_msg initiators);
+          val _ = member (op =) initiators theory_name andalso error (cycle_msg initiators);
 
-          val (current, deps, theory_pos, imports, keywords) = check_deps dir' name
+          val (current, deps, theory_pos, imports, keywords) = check_deps master_dir theory_name
             handle ERROR msg =>
               cat_error msg
-                ("The error(s) above occurred for theory " ^ quote name ^
+                ("The error(s) above occurred for theory " ^ quote theory_name ^
                   Position.here require_pos ^ required_by "\n" initiators);
 
-          val parents = map (base_name o #1) imports;
+          val qualifier' = Resources.theory_qualifier theory_name;
+          val dir' = Path.append dir (master_dir_deps (Option.map #1 deps));
+
+          val parents = map (#theory_name o Resources.import_name qualifier' dir' o #1) imports;
           val (parents_current, tasks') =
-            require_thys document symbols last_timing (name :: initiators)
-              (Path.append dir (master_dir (Option.map #1 deps))) imports tasks;
+            require_thys document symbols last_timing (theory_name :: initiators)
+              qualifier' dir' imports tasks;
 
           val all_current = current andalso parents_current;
           val task =
-            if all_current then Finished (get_theory name)
+            if all_current then Finished (get_theory theory_name)
             else
               (case deps of
                 NONE => raise Fail "Malformed deps"
@@ -332,28 +331,29 @@
                     val update_time = serial ();
                     val load =
                       load_thy document symbols last_timing initiators update_time dep
-                        text (name, theory_pos) keywords;
+                        text (theory_name, theory_pos) keywords;
                   in Task (node_name, parents, load) end);
 
-          val tasks'' = new_entry name parents task tasks';
+          val tasks'' = new_entry theory_name parents task tasks';
         in (all_current, tasks'') end)
   end;
 
 end;
 
 
-(* use_thy *)
+(* use theories *)
 
-fun use_theories {document, symbols, last_timing, master_dir} imports =
-  schedule_tasks
-    (snd (require_thys document symbols last_timing [] master_dir imports String_Graph.empty));
+fun use_theories {document, symbols, last_timing, qualifier, master_dir} imports =
+  let
+    val (_, tasks) =
+      require_thys document symbols last_timing [] qualifier master_dir imports String_Graph.empty;
+  in schedule_tasks tasks end;
 
-val use_thys =
+fun use_thy name =
   use_theories
     {document = false, symbols = HTML.no_symbols, last_timing = K Time.zeroTime,
-      master_dir = Path.current};
-
-val use_thy = use_thys o single;
+     qualifier = Resources.default_qualifier (), master_dir = Path.current}
+    [(name, Position.none)];
 
 
 (* toplevel scripting -- without maintaining database *)
@@ -372,7 +372,7 @@
 
 fun register_thy theory =
   let
-    val name = Context.theory_name theory;
+    val name = Context.theory_long_name theory;
     val {master, ...} = Resources.check_thy (Resources.master_directory theory) name;
     val imports = Resources.imports_of theory;
   in
@@ -390,4 +390,4 @@
 
 end;
 
-fun use_thy name = Runtime.toplevel_program (fn () => Thy_Info.use_thy (name, Position.none));
+fun use_thy name = Runtime.toplevel_program (fn () => Thy_Info.use_thy name);
diff -r f556a7a9080c -r f3cd78ba687c src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Pure/Thy/thy_info.scala	Wed Apr 12 13:48:07 2017 +0200
@@ -85,7 +85,7 @@
         case (loaded, dep) =>
           val name = dep.name.loaded_theory
           loaded + (name.theory -> name) +
-            (Long_Name.base_name(name.theory) -> name)  // legacy
+            (name.theory_base_name -> name)  // legacy
       }
 
     def loaded_files: List[Path] =
@@ -108,7 +108,7 @@
 
       def node(name: Document.Node.Name): Graph_Display.Node =
         if (parent_base.loaded_theory(name)) parent_session_node
-        else Graph_Display.Node(Long_Name.base_name(name.theory), "theory." + name.theory)
+        else Graph_Display.Node(name.theory_base_name, "theory." + name.theory)
 
       (Graph_Display.empty_graph /: deps) {
         case (g, dep) =>
diff -r f556a7a9080c -r f3cd78ba687c src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Pure/Tools/build.ML	Wed Apr 12 13:48:07 2017 +0200
@@ -101,7 +101,7 @@
 
 (* build theories *)
 
-fun build_theories symbols last_timing master_dir (options, thys) =
+fun build_theories symbols last_timing qualifier master_dir (options, thys) =
   let
     val condition = space_explode "," (Options.string options "condition");
     val conds = filter_out (can getenv_strict) condition;
@@ -115,6 +115,7 @@
           document = Present.document_enabled (Options.string options "document"),
           symbols = symbols,
           last_timing = last_timing,
+          qualifier = qualifier,
           master_dir = master_dir}
         |>
           (case Options.string options "profiling" of
@@ -145,6 +146,8 @@
   name: string,
   master_dir: Path.T,
   theories: (Options.T * (string * Position.T) list) list,
+  global_theories: (string * string) list,
+  loaded_theories: (string * string) list,
   known_theories: (string * string) list};
 
 fun decode_args yxml =
@@ -152,12 +155,13 @@
     open XML.Decode;
     val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
       (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir,
-      (theories, known_theories)))))))))))) =
+      (theories, (global_theories, (loaded_theories, known_theories)))))))))))))) =
       pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string
         (pair (list (pair string string)) (pair string (pair string (pair string (pair string
           (pair string
             (pair (((list (pair Options.decode (list (string #> rpair Position.none))))))
-              (list (pair string string)))))))))))))
+              (pair (list (pair string string))
+                (pair (list (pair string string)) (list (pair string string)))))))))))))))
       (YXML.parse_body yxml);
   in
     Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
@@ -165,15 +169,22 @@
       document_files = map (apply2 Path.explode) document_files,
       graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter,
       name = name, master_dir = Path.explode master_dir, theories = theories,
+      global_theories = global_theories, loaded_theories = loaded_theories,
       known_theories = known_theories}
   end;
 
 fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info,
-    document_files, graph_file, parent_name, chapter, name, master_dir, theories, known_theories}) =
+    document_files, graph_file, parent_name, chapter, name, master_dir, theories,
+    global_theories, loaded_theories, known_theories}) =
   let
     val symbols = HTML.make_symbols symbol_codes;
 
-    val _ = Resources.set_session_base {known_theories = known_theories};
+    val _ =
+      Resources.set_session_base
+        {default_qualifier = name,
+         global_theories = global_theories,
+         loaded_theories = loaded_theories,
+         known_theories = known_theories};
 
     val _ =
       Session.init
@@ -194,7 +205,7 @@
 
     val res1 =
       theories |>
-        (List.app (build_theories symbols last_timing master_dir)
+        (List.app (build_theories symbols last_timing name master_dir)
           |> session_timing name verbose
           |> Exn.capture);
     val res2 = Exn.capture Session.finish ();
diff -r f556a7a9080c -r f3cd78ba687c src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Pure/Tools/build.scala	Wed Apr 12 13:48:07 2017 +0200
@@ -196,7 +196,7 @@
     private val future_result: Future[Process_Result] =
       Future.thread("build") {
         val parent = info.parent.getOrElse("")
-
+        val base = deps(name)
         val args_yxml =
           YXML.string_of_body(
             {
@@ -205,12 +205,14 @@
                 pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
                 pair(string, pair(string, pair(string, pair(Path.encode,
                 pair(list(pair(Options.encode, list(string))),
-                list(pair(string, string))))))))))))))(
+                pair(list(pair(string, string)),
+                pair(list(pair(string, string)), list(pair(string, string))))))))))))))))(
               (Symbol.codes, (command_timings, (do_output, (verbose,
                 (store.browser_info, (info.document_files, (File.standard_path(graph_file),
                 (parent, (info.chapter, (name, (Path.current,
                 (info.theories,
-                deps(name).dest_known_theories)))))))))))))
+                (base.global_theories.toList,
+                (base.dest_loaded_theories, base.dest_known_theories)))))))))))))))
             })
 
         val env =
@@ -222,7 +224,8 @@
             ML_Syntax.print_string0(File.platform_path(output))
 
         if (pide && !Sessions.is_pure(name)) {
-          val resources = new Resources(name, deps(parent))
+          val resources =
+            new Resources(deps(parent), default_qualifier = info.theory_qualifier(name))
           val session = new Session(options, resources)
           val handler = new Handler(progress, session, name)
           session.init_protocol_handler(handler)
diff -r f556a7a9080c -r f3cd78ba687c src/Pure/Tools/ml_process.scala
--- a/src/Pure/Tools/ml_process.scala	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Pure/Tools/ml_process.scala	Wed Apr 12 13:48:07 2017 +0200
@@ -95,10 +95,14 @@
       session_base match {
         case None => Nil
         case Some(base) =>
-          List("Resources.set_session_base {known_theories = " +
+          def print_table(table: List[(String, String)]): String =
             ML_Syntax.print_list(
               ML_Syntax.print_pair(
-                ML_Syntax.print_string, ML_Syntax.print_string))(base.dest_known_theories) + "}")
+                ML_Syntax.print_string, ML_Syntax.print_string))(table)
+          List("Resources.set_session_base {default_qualifier = \"\"" +
+            ", global_theories = " + print_table(base.global_theories.toList) +
+            ", loaded_theories = " + print_table(base.dest_loaded_theories) +
+            ", known_theories = " + print_table(base.dest_known_theories) + "}")
       }
 
     // process
diff -r f556a7a9080c -r f3cd78ba687c src/Pure/context.ML
--- a/src/Pure/context.ML	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Pure/context.ML	Wed Apr 12 13:48:07 2017 +0200
@@ -33,7 +33,9 @@
   val timing: bool Unsynchronized.ref
   val parents_of: theory -> theory list
   val ancestors_of: theory -> theory list
+  val theory_id_long_name: theory_id -> string
   val theory_id_name: theory_id -> string
+  val theory_long_name: theory -> string
   val theory_name: theory -> string
   val PureN: string
   val pretty_thy: theory -> Pretty.T
@@ -148,8 +150,11 @@
 fun make_history name stage = {name = name, stage = stage};
 fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors};
 
-val theory_id_name = #name o history_of_id;
-val theory_name = #name o history_of;
+val theory_id_long_name = #name o history_of_id;
+val theory_id_name = Long_Name.base_name o theory_id_long_name;
+val theory_long_name = #name o history_of;
+val theory_name = Long_Name.base_name o theory_long_name;
+
 val parents_of = #parents o ancestry_of;
 val ancestors_of = #ancestors o ancestry_of;
 
@@ -160,7 +165,9 @@
 val finished = ~1;
 
 fun display_name thy_id =
-  let val {name, stage} = history_of_id thy_id
+  let
+    val {name = long_name, stage} = history_of_id thy_id;
+    val name = Long_Name.base_name long_name;
   in if stage = finished then name else name ^ ":" ^ string_of_int stage end;
 
 fun display_names thy =
diff -r f556a7a9080c -r f3cd78ba687c src/Pure/global_theory.ML
--- a/src/Pure/global_theory.ML	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Pure/global_theory.ML	Wed Apr 12 13:48:07 2017 +0200
@@ -80,7 +80,7 @@
       fold (fn thy' => Symtab.update (Context.theory_name thy', thy'))
         (Theory.nodes_of thy) Symtab.empty;
     fun transfer th =
-      Thm.transfer (the_default thy (Symtab.lookup theories (Thm.theory_name_of_thm th))) th;
+      Thm.transfer (the_default thy (Symtab.lookup theories (Thm.theory_name th))) th;
   in transfer end;
 
 fun all_thms_of thy verbose =
diff -r f556a7a9080c -r f3cd78ba687c src/Pure/goal.ML
--- a/src/Pure/goal.ML	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Pure/goal.ML	Wed Apr 12 13:48:07 2017 +0200
@@ -210,7 +210,7 @@
       | SOME st =>
           let
             val _ =
-              Context.subthy_id (Thm.theory_id_of_thm st, Context.theory_id thy) orelse
+              Context.subthy_id (Thm.theory_id st, Context.theory_id thy) orelse
                 err "Bad background theory of goal state";
             val res =
               (finish ctxt' st
diff -r f556a7a9080c -r f3cd78ba687c src/Pure/more_thm.ML
--- a/src/Pure/more_thm.ML	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Pure/more_thm.ML	Wed Apr 12 13:48:07 2017 +0200
@@ -216,7 +216,7 @@
 
 fun eq_thm_strict ths =
   eq_thm ths andalso
-  Context.eq_thy_id (apply2 Thm.theory_id_of_thm ths) andalso
+  Context.eq_thy_id (apply2 Thm.theory_id ths) andalso
   op = (apply2 Thm.maxidx_of ths) andalso
   op = (apply2 Thm.get_tags ths);
 
diff -r f556a7a9080c -r f3cd78ba687c src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Pure/proofterm.ML	Wed Apr 12 13:48:07 2017 +0200
@@ -8,8 +8,6 @@
 
 signature BASIC_PROOFTERM =
 sig
-  val proofs: int Unsynchronized.ref
-
   type thm_node
   datatype proof =
      MinProof
@@ -28,14 +26,13 @@
     {oracles: (string * term) Ord_List.T,
      thms: (serial * thm_node) Ord_List.T,
      proof: proof}
-
   val %> : proof * term -> proof
 end;
 
 signature PROOFTERM =
 sig
   include BASIC_PROOFTERM
-
+  val proofs: int Unsynchronized.ref
   type pthm = serial * thm_node
   type oracle = string * term
   val proof_of: proof_body -> proof
diff -r f556a7a9080c -r f3cd78ba687c src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Pure/thm.ML	Wed Apr 12 13:48:07 2017 +0200
@@ -56,8 +56,8 @@
   val fold_atomic_cterms: (cterm -> 'a -> 'a) -> thm -> 'a -> 'a
   val terms_of_tpairs: (term * term) list -> term list
   val full_prop_of: thm -> term
-  val theory_id_of_thm: thm -> Context.theory_id
-  val theory_name_of_thm: thm -> string
+  val theory_id: thm -> Context.theory_id
+  val theory_name: thm -> string
   val maxidx_of: thm -> int
   val maxidx_thm: thm -> int -> int
   val shyps_of: thm -> sort Ord_List.T
@@ -365,8 +365,8 @@
 (* basic components *)
 
 val cert_of = #cert o rep_thm;
-val theory_id_of_thm = Context.certificate_theory_id o cert_of;
-val theory_name_of_thm = Context.theory_id_name o theory_id_of_thm;
+val theory_id = Context.certificate_theory_id o cert_of;
+val theory_name = Context.theory_id_name o theory_id;
 
 val maxidx_of = #maxidx o rep_thm;
 fun maxidx_thm th i = Int.max (maxidx_of th, i);
diff -r f556a7a9080c -r f3cd78ba687c src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Wed Apr 12 13:48:07 2017 +0200
@@ -43,7 +43,7 @@
     val options: Options,
     session_base: Sessions.Base,
     log: Logger = No_Logger)
-  extends Resources(session_name = "", session_base, log)
+  extends Resources(session_base, log = log)
 {
   private val state = Synchronized(VSCode_Resources.State())
 
@@ -63,7 +63,7 @@
   def node_name(file: JFile): Document.Node.Name =
   {
     val node = file.getPath
-    val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("")
+    val theory = Thy_Header.theory_name(node)
     val master_dir = if (theory == "") "" else file.getParent
     Document.Node.Name(node, master_dir, theory)
   }
diff -r f556a7a9080c -r f3cd78ba687c src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Wed Apr 12 13:48:07 2017 +0200
@@ -21,15 +21,14 @@
 import org.gjt.sp.jedit.bufferio.BufferIORequest
 
 
-class JEdit_Resources(session_base: Sessions.Base)
-  extends Resources(session_name = "", session_base)
+class JEdit_Resources(session_base: Sessions.Base) extends Resources(session_base)
 {
   /* document node name */
 
   def node_name(buffer: Buffer): Document.Node.Name =
   {
     val node = JEdit_Lib.buffer_name(buffer)
-    val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("")
+    val theory = Thy_Header.theory_name(node)
     val master_dir = if (theory == "") "" else buffer.getDirectory
     Document.Node.Name(node, master_dir, theory)
   }
@@ -38,7 +37,7 @@
   {
     val vfs = VFSManager.getVFSForPath(path)
     val node = if (vfs.isInstanceOf[FileVFS]) MiscUtilities.resolveSymlinks(path) else path
-    val theory = Thy_Header.thy_name_bootstrap(node).getOrElse("")
+    val theory = Thy_Header.theory_name(node)
     val master_dir = if (theory == "") "" else vfs.getParentOfPath(path)
     Document.Node.Name(node, master_dir, theory)
   }
diff -r f556a7a9080c -r f3cd78ba687c src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Apr 12 13:48:07 2017 +0200
@@ -76,9 +76,7 @@
       try { Sessions.session_base(options, session_name, JEdit_Sessions.session_dirs()) }
       catch { case ERROR(_) => Sessions.Base.pure(options) }
 
-    _resources =
-      new JEdit_Resources(session_base.copy(known_theories =
-        for ((a, b) <- session_base.known_theories) yield (a, b.map(File.platform_path(_)))))
+    _resources = new JEdit_Resources(session_base.platform_path)
   }
   def resources: JEdit_Resources = _resources
 
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/AC.thy
--- a/src/ZF/AC.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/AC.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -5,7 +5,7 @@
 
 section\<open>The Axiom of Choice\<close>
 
-theory AC imports Main_ZF begin
+theory AC imports ZF begin
 
 text\<open>This definition comes from Halmos (1960), page 59.\<close>
 axiomatization where
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/AC/AC_Equiv.thy
--- a/src/ZF/AC/AC_Equiv.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/AC/AC_Equiv.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -12,8 +12,8 @@
 *)
 
 theory AC_Equiv
-imports Main
-begin (*obviously not Main_ZFC*)
+imports ZF
+begin (*obviously not ZFC*)
 
 (* Well Ordering Theorems *)
 
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/Coind/Language.thy
--- a/src/ZF/Coind/Language.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/Coind/Language.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -3,7 +3,7 @@
     Copyright   1995  University of Cambridge
 *)
 
-theory Language imports Main begin
+theory Language imports ZF begin
 
 
 text\<open>these really can't be definitions without losing the abstraction\<close>
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/Coind/Map.thy
--- a/src/ZF/Coind/Map.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/Coind/Map.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -5,7 +5,7 @@
 Some sample proofs of inclusions for the final coalgebra "U" (by lcp).
 *)
 
-theory Map imports Main begin
+theory Map imports ZF begin
 
 definition
   TMap :: "[i,i] => i"  where
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/Constructible/Formula.thy
--- a/src/ZF/Constructible/Formula.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/Constructible/Formula.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -4,7 +4,7 @@
 
 section \<open>First-Order Formulas and the Definition of the Class L\<close>
 
-theory Formula imports Main begin
+theory Formula imports ZF begin
 
 subsection\<open>Internalized formulas of FOL\<close>
 
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/Constructible/MetaExists.thy
--- a/src/ZF/Constructible/MetaExists.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/Constructible/MetaExists.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -4,7 +4,7 @@
 
 section\<open>The meta-existential quantifier\<close>
 
-theory MetaExists imports Main begin
+theory MetaExists imports ZF begin
 
 text\<open>Allows quantification over any term.  Used to quantify over classes.
 Yields a proposition rather than a FOL formula.\<close>
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/Constructible/Normal.thy
--- a/src/ZF/Constructible/Normal.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/Constructible/Normal.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -4,7 +4,7 @@
 
 section \<open>Closed Unbounded Classes and Normal Functions\<close>
 
-theory Normal imports Main begin
+theory Normal imports ZF begin
 
 text\<open>
 One source is the book
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/Constructible/Relative.thy
--- a/src/ZF/Constructible/Relative.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/Constructible/Relative.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -4,7 +4,7 @@
 
 section \<open>Relativization and Absoluteness\<close>
 
-theory Relative imports Main begin
+theory Relative imports ZF begin
 
 subsection\<open>Relativized versions of standard set-theoretic concepts\<close>
 
@@ -593,13 +593,13 @@
 
 lemma (in M_trivial) pair_abs [simp]:
      "M(z) ==> pair(M,a,b,z) \<longleftrightarrow> z=<a,b>"
-apply (simp add: pair_def ZF.Pair_def)
+apply (simp add: pair_def Pair_def)
 apply (blast intro: transM)
 done
 
 lemma (in M_trivial) pair_in_M_iff [iff]:
      "M(<a,b>) \<longleftrightarrow> M(a) & M(b)"
-by (simp add: ZF.Pair_def)
+by (simp add: Pair_def)
 
 lemma (in M_trivial) pair_components_in_M:
      "[| <x,y> \<in> A; M(A) |] ==> M(x) & M(y)"
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/IMP/Com.thy
--- a/src/ZF/IMP/Com.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/IMP/Com.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -4,7 +4,7 @@
 
 section \<open>Arithmetic expressions, boolean expressions, commands\<close>
 
-theory Com imports Main begin
+theory Com imports ZF begin
 
 
 subsection \<open>Arithmetic expressions\<close>
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/Induct/Acc.thy
--- a/src/ZF/Induct/Acc.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/Induct/Acc.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -5,7 +5,7 @@
 
 section \<open>The accessible part of a relation\<close>
 
-theory Acc imports Main begin
+theory Acc imports ZF begin
 
 text \<open>
   Inductive definition of \<open>acc(r)\<close>; see @{cite "paulin-tlca"}.
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/Induct/Binary_Trees.thy
--- a/src/ZF/Induct/Binary_Trees.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/Induct/Binary_Trees.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -5,7 +5,7 @@
 
 section \<open>Binary trees\<close>
 
-theory Binary_Trees imports Main begin
+theory Binary_Trees imports ZF begin
 
 subsection \<open>Datatype definition\<close>
 
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/Induct/Brouwer.thy
--- a/src/ZF/Induct/Brouwer.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/Induct/Brouwer.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -5,7 +5,7 @@
 
 section \<open>Infinite branching datatype definitions\<close>
 
-theory Brouwer imports Main_ZFC begin
+theory Brouwer imports ZFC begin
 
 subsection \<open>The Brouwer ordinals\<close>
 
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/Induct/Comb.thy
--- a/src/ZF/Induct/Comb.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/Induct/Comb.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -6,7 +6,7 @@
 section \<open>Combinatory Logic example: the Church-Rosser Theorem\<close>
 
 theory Comb
-imports Main
+imports ZF
 begin
 
 text \<open>
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/Induct/Datatypes.thy
--- a/src/ZF/Induct/Datatypes.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/Induct/Datatypes.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -5,7 +5,7 @@
 
 section \<open>Sample datatype definitions\<close>
 
-theory Datatypes imports Main begin
+theory Datatypes imports ZF begin
 
 subsection \<open>A type with four constructors\<close>
 
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/Induct/FoldSet.thy
--- a/src/ZF/Induct/FoldSet.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/Induct/FoldSet.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -6,7 +6,7 @@
 least left-commutative.  
 *)
 
-theory FoldSet imports Main begin
+theory FoldSet imports ZF begin
 
 consts fold_set :: "[i, i, [i,i]=>i, i] => i"
 
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/Induct/ListN.thy
--- a/src/ZF/Induct/ListN.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/Induct/ListN.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -5,7 +5,7 @@
 
 section \<open>Lists of n elements\<close>
 
-theory ListN imports Main begin
+theory ListN imports ZF begin
 
 text \<open>
   Inductive definition of lists of \<open>n\<close> elements; see
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/Induct/Mutil.thy
--- a/src/ZF/Induct/Mutil.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/Induct/Mutil.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -5,7 +5,7 @@
 
 section \<open>The Mutilated Chess Board Problem, formalized inductively\<close>
 
-theory Mutil imports Main begin
+theory Mutil imports ZF begin
 
 text \<open>
   Originator is Max Black, according to J A Robinson.  Popularized as
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/Induct/Ntree.thy
--- a/src/ZF/Induct/Ntree.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/Induct/Ntree.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -5,7 +5,7 @@
 
 section \<open>Datatype definition n-ary branching trees\<close>
 
-theory Ntree imports Main begin
+theory Ntree imports ZF begin
 
 text \<open>
   Demonstrates a simple use of function space in a datatype
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/Induct/Primrec.thy
--- a/src/ZF/Induct/Primrec.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/Induct/Primrec.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -5,7 +5,7 @@
 
 section \<open>Primitive Recursive Functions: the inductive definition\<close>
 
-theory Primrec imports Main begin
+theory Primrec imports ZF begin
 
 text \<open>
   Proof adopted from @{cite szasz93}.
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/Induct/PropLog.thy
--- a/src/ZF/Induct/PropLog.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/Induct/PropLog.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -5,7 +5,7 @@
 
 section \<open>Meta-theory of propositional logic\<close>
 
-theory PropLog imports Main begin
+theory PropLog imports ZF begin
 
 text \<open>
   Datatype definition of propositional logic formulae and inductive
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/Induct/Rmap.thy
--- a/src/ZF/Induct/Rmap.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/Induct/Rmap.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -5,7 +5,7 @@
 
 section \<open>An operator to ``map'' a relation over a list\<close>
 
-theory Rmap imports Main begin
+theory Rmap imports ZF begin
 
 consts
   rmap :: "i=>i"
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/Induct/Term.thy
--- a/src/ZF/Induct/Term.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/Induct/Term.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -5,7 +5,7 @@
 
 section \<open>Terms over an alphabet\<close>
 
-theory Term imports Main begin
+theory Term imports ZF begin
 
 text \<open>
   Illustrates the list functor (essentially the same type as in \<open>Trees_Forest\<close>).
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/Induct/Tree_Forest.thy
--- a/src/ZF/Induct/Tree_Forest.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/Induct/Tree_Forest.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -5,7 +5,7 @@
 
 section \<open>Trees and forests, a mutually recursive type definition\<close>
 
-theory Tree_Forest imports Main begin
+theory Tree_Forest imports ZF begin
 
 subsection \<open>Datatype definition\<close>
 
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/Main.thy
--- a/src/ZF/Main.thy	Tue Apr 11 10:29:25 2017 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,5 +0,0 @@
-theory Main 
-imports Main_ZF
-begin
-
-end
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/Main_ZF.thy
--- a/src/ZF/Main_ZF.thy	Tue Apr 11 10:29:25 2017 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,73 +0,0 @@
-section\<open>Theory Main: Everything Except AC\<close>
-
-theory Main_ZF imports List_ZF IntDiv_ZF CardinalArith begin
-
-(*The theory of "iterates" logically belongs to Nat, but can't go there because
-  primrec isn't available into after Datatype.*)
-
-subsection\<open>Iteration of the function @{term F}\<close>
-
-consts  iterates :: "[i=>i,i,i] => i"   ("(_^_ '(_'))" [60,1000,1000] 60)
-
-primrec
-    "F^0 (x) = x"
-    "F^(succ(n)) (x) = F(F^n (x))"
-
-definition
-  iterates_omega :: "[i=>i,i] => i" ("(_^\<omega> '(_'))" [60,1000] 60) where
-    "F^\<omega> (x) == \<Union>n\<in>nat. F^n (x)"
-
-lemma iterates_triv:
-     "[| n\<in>nat;  F(x) = x |] ==> F^n (x) = x"
-by (induct n rule: nat_induct, simp_all)
-
-lemma iterates_type [TC]:
-     "[| n \<in> nat;  a \<in> A; !!x. x \<in> A ==> F(x) \<in> A |]
-      ==> F^n (a) \<in> A"
-by (induct n rule: nat_induct, simp_all)
-
-lemma iterates_omega_triv:
-    "F(x) = x ==> F^\<omega> (x) = x"
-by (simp add: iterates_omega_def iterates_triv)
-
-lemma Ord_iterates [simp]:
-     "[| n\<in>nat;  !!i. Ord(i) ==> Ord(F(i));  Ord(x) |]
-      ==> Ord(F^n (x))"
-by (induct n rule: nat_induct, simp_all)
-
-lemma iterates_commute: "n \<in> nat ==> F(F^n (x)) = F^n (F(x))"
-by (induct_tac n, simp_all)
-
-
-subsection\<open>Transfinite Recursion\<close>
-
-text\<open>Transfinite recursion for definitions based on the
-    three cases of ordinals\<close>
-
-definition
-  transrec3 :: "[i, i, [i,i]=>i, [i,i]=>i] =>i" where
-    "transrec3(k, a, b, c) ==
-       transrec(k, \<lambda>x r.
-         if x=0 then a
-         else if Limit(x) then c(x, \<lambda>y\<in>x. r`y)
-         else b(Arith.pred(x), r ` Arith.pred(x)))"
-
-lemma transrec3_0 [simp]: "transrec3(0,a,b,c) = a"
-by (rule transrec3_def [THEN def_transrec, THEN trans], simp)
-
-lemma transrec3_succ [simp]:
-     "transrec3(succ(i),a,b,c) = b(i, transrec3(i,a,b,c))"
-by (rule transrec3_def [THEN def_transrec, THEN trans], simp)
-
-lemma transrec3_Limit:
-     "Limit(i) ==>
-      transrec3(i,a,b,c) = c(i, \<lambda>j\<in>i. transrec3(j,a,b,c))"
-by (rule transrec3_def [THEN def_transrec, THEN trans], force)
-
-
-declaration \<open>fn _ =>
-  Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt =>
-    map mk_eq o Ord_atomize o Variable.gen_all ctxt))
-\<close>
-
-end
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/Main_ZFC.thy
--- a/src/ZF/Main_ZFC.thy	Tue Apr 11 10:29:25 2017 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,4 +0,0 @@
-theory Main_ZFC imports Main_ZF InfDatatype
-begin
-
-end
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/ROOT
--- a/src/ZF/ROOT	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/ROOT	Wed Apr 12 13:48:07 2017 +0200
@@ -43,8 +43,7 @@
     (North-Holland, 1980)
   *}
   theories
-    Main
-    Main_ZFC
+    ZFC
   document_files "root.tex"
 
 session "ZF-AC" (ZF) in AC = ZF +
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/Resid/Redex.thy
--- a/src/ZF/Resid/Redex.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/Resid/Redex.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -2,7 +2,7 @@
     Author:     Ole Rasmussen, University of Cambridge
 *)
 
-theory Redex imports Main begin
+theory Redex imports ZF begin
 consts
   redexes     :: i
 
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/UNITY/GenPrefix.thy
--- a/src/ZF/UNITY/GenPrefix.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/UNITY/GenPrefix.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -12,7 +12,7 @@
 section\<open>Charpentier's Generalized Prefix Relation\<close>
 
 theory GenPrefix
-imports Main
+imports ZF
 begin
 
 definition (*really belongs in ZF/Trancl*)
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/UNITY/State.thy
--- a/src/ZF/UNITY/State.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/UNITY/State.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -10,7 +10,7 @@
 
 section\<open>UNITY Program States\<close>
 
-theory State imports Main begin
+theory State imports ZF begin
 
 consts var :: i
 datatype var = Var("i \<in> list(nat)")
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/UNITY/WFair.thy
--- a/src/ZF/UNITY/WFair.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/UNITY/WFair.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -6,7 +6,7 @@
 section\<open>Progress under Weak Fairness\<close>
 
 theory WFair
-imports UNITY Main_ZFC
+imports UNITY ZFC
 begin
 
 text\<open>This theory defines the operators transient, ensures and leadsTo,
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/ZF.thy
--- a/src/ZF/ZF.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/ZF.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -1,650 +1,73 @@
-(*  Title:      ZF/ZF.thy
-    Author:     Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
-    Copyright   1993  University of Cambridge
-*)
-
-section \<open>Zermelo-Fraenkel Set Theory\<close>
-
-theory ZF
-imports "~~/src/FOL/FOL"
-begin
-
-subsection \<open>Signature\<close>
-
-declare [[eta_contract = false]]
+section\<open>Main ZF Theory: Everything Except AC\<close>
 
-typedecl i
-instance i :: "term" ..
-
-axiomatization mem :: "[i, i] \<Rightarrow> o"  (infixl "\<in>" 50)  \<comment> \<open>membership relation\<close>
-  and zero :: "i"  ("0")  \<comment> \<open>the empty set\<close>
-  and Pow :: "i \<Rightarrow> i"  \<comment> \<open>power sets\<close>
-  and Inf :: "i"  \<comment> \<open>infinite set\<close>
-  and Union :: "i \<Rightarrow> i"  ("\<Union>_" [90] 90)
-  and PrimReplace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i"
-
-abbreviation not_mem :: "[i, i] \<Rightarrow> o"  (infixl "\<notin>" 50)  \<comment> \<open>negated membership relation\<close>
-  where "x \<notin> y \<equiv> \<not> (x \<in> y)"
-
-
-subsection \<open>Bounded Quantifiers\<close>
-
-definition Ball :: "[i, i \<Rightarrow> o] \<Rightarrow> o"
-  where "Ball(A, P) \<equiv> \<forall>x. x\<in>A \<longrightarrow> P(x)"
+theory ZF imports List_ZF IntDiv_ZF CardinalArith begin
 
-definition Bex :: "[i, i \<Rightarrow> o] \<Rightarrow> o"
-  where "Bex(A, P) \<equiv> \<exists>x. x\<in>A \<and> P(x)"
-
-syntax
-  "_Ball" :: "[pttrn, i, o] \<Rightarrow> o"  ("(3\<forall>_\<in>_./ _)" 10)
-  "_Bex" :: "[pttrn, i, o] \<Rightarrow> o"  ("(3\<exists>_\<in>_./ _)" 10)
-translations
-  "\<forall>x\<in>A. P" \<rightleftharpoons> "CONST Ball(A, \<lambda>x. P)"
-  "\<exists>x\<in>A. P" \<rightleftharpoons> "CONST Bex(A, \<lambda>x. P)"
-
-
-subsection \<open>Variations on Replacement\<close>
+(*The theory of "iterates" logically belongs to Nat, but can't go there because
+  primrec isn't available into after Datatype.*)
 
-(* Derived form of replacement, restricting P to its functional part.
-   The resulting set (for functional P) is the same as with
-   PrimReplace, but the rules are simpler. *)
-definition Replace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i"
-  where "Replace(A,P) == PrimReplace(A, %x y. (\<exists>!z. P(x,z)) & P(x,y))"
-
-syntax
-  "_Replace"  :: "[pttrn, pttrn, i, o] => i"  ("(1{_ ./ _ \<in> _, _})")
-translations
-  "{y. x\<in>A, Q}" \<rightleftharpoons> "CONST Replace(A, \<lambda>x y. Q)"
-
-
-(* Functional form of replacement -- analgous to ML's map functional *)
-
-definition RepFun :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
-  where "RepFun(A,f) == {y . x\<in>A, y=f(x)}"
-
-syntax
-  "_RepFun" :: "[i, pttrn, i] => i"  ("(1{_ ./ _ \<in> _})" [51,0,51])
-translations
-  "{b. x\<in>A}" \<rightleftharpoons> "CONST RepFun(A, \<lambda>x. b)"
-
+subsection\<open>Iteration of the function @{term F}\<close>
 
-(* Separation and Pairing can be derived from the Replacement
-   and Powerset Axioms using the following definitions. *)
-definition Collect :: "[i, i \<Rightarrow> o] \<Rightarrow> i"
-  where "Collect(A,P) == {y . x\<in>A, x=y & P(x)}"
-
-syntax
-  "_Collect" :: "[pttrn, i, o] \<Rightarrow> i"  ("(1{_ \<in> _ ./ _})")
-translations
-  "{x\<in>A. P}" \<rightleftharpoons> "CONST Collect(A, \<lambda>x. P)"
-
-
-subsection \<open>General union and intersection\<close>
-
-definition Inter :: "i => i"  ("\<Inter>_" [90] 90)
-  where "\<Inter>(A) == { x\<in>\<Union>(A) . \<forall>y\<in>A. x\<in>y}"
-
-syntax
-  "_UNION" :: "[pttrn, i, i] => i"  ("(3\<Union>_\<in>_./ _)" 10)
-  "_INTER" :: "[pttrn, i, i] => i"  ("(3\<Inter>_\<in>_./ _)" 10)
-translations
-  "\<Union>x\<in>A. B" == "CONST Union({B. x\<in>A})"
-  "\<Inter>x\<in>A. B" == "CONST Inter({B. x\<in>A})"
-
-
-subsection \<open>Finite sets and binary operations\<close>
-
-(*Unordered pairs (Upair) express binary union/intersection and cons;
-  set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*)
-
-definition Upair :: "[i, i] => i"
-  where "Upair(a,b) == {y. x\<in>Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)}"
-
-definition Subset :: "[i, i] \<Rightarrow> o"  (infixl "\<subseteq>" 50)  \<comment> \<open>subset relation\<close>
-  where subset_def: "A \<subseteq> B \<equiv> \<forall>x\<in>A. x\<in>B"
+consts  iterates :: "[i=>i,i,i] => i"   ("(_^_ '(_'))" [60,1000,1000] 60)
 
-definition Diff :: "[i, i] \<Rightarrow> i"  (infixl "-" 65)  \<comment> \<open>set difference\<close>
-  where "A - B == { x\<in>A . ~(x\<in>B) }"
-
-definition Un :: "[i, i] \<Rightarrow> i"  (infixl "\<union>" 65)  \<comment> \<open>binary union\<close>
-  where "A \<union> B == \<Union>(Upair(A,B))"
-
-definition Int :: "[i, i] \<Rightarrow> i"  (infixl "\<inter>" 70)  \<comment> \<open>binary intersection\<close>
-  where "A \<inter> B == \<Inter>(Upair(A,B))"
-
-definition cons :: "[i, i] => i"
-  where "cons(a,A) == Upair(a,a) \<union> A"
-
-definition succ :: "i => i"
-  where "succ(i) == cons(i, i)"
+primrec
+    "F^0 (x) = x"
+    "F^(succ(n)) (x) = F(F^n (x))"
 
-nonterminal "is"
-syntax
-  "" :: "i \<Rightarrow> is"  ("_")
-  "_Enum" :: "[i, is] \<Rightarrow> is"  ("_,/ _")
-  "_Finset" :: "is \<Rightarrow> i"  ("{(_)}")
-translations
-  "{x, xs}" == "CONST cons(x, {xs})"
-  "{x}" == "CONST cons(x, 0)"
-
-
-subsection \<open>Axioms\<close>
-
-(* ZF axioms -- see Suppes p.238
-   Axioms for Union, Pow and Replace state existence only,
-   uniqueness is derivable using extensionality. *)
-
-axiomatization
-where
-  extension:     "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" and
-  Union_iff:     "A \<in> \<Union>(C) \<longleftrightarrow> (\<exists>B\<in>C. A\<in>B)" and
-  Pow_iff:       "A \<in> Pow(B) \<longleftrightarrow> A \<subseteq> B" and
-
-  (*We may name this set, though it is not uniquely defined.*)
-  infinity:      "0 \<in> Inf \<and> (\<forall>y\<in>Inf. succ(y) \<in> Inf)" and
+definition
+  iterates_omega :: "[i=>i,i] => i" ("(_^\<omega> '(_'))" [60,1000] 60) where
+    "F^\<omega> (x) == \<Union>n\<in>nat. F^n (x)"
 
-  (*This formulation facilitates case analysis on A.*)
-  foundation:    "A = 0 \<or> (\<exists>x\<in>A. \<forall>y\<in>x. y\<notin>A)" and
-
-  (*Schema axiom since predicate P is a higher-order variable*)
-  replacement:   "(\<forall>x\<in>A. \<forall>y z. P(x,y) \<and> P(x,z) \<longrightarrow> y = z) \<Longrightarrow>
-                         b \<in> PrimReplace(A,P) \<longleftrightarrow> (\<exists>x\<in>A. P(x,b))"
-
-
-subsection \<open>Definite descriptions -- via Replace over the set "1"\<close>
-
-definition The :: "(i \<Rightarrow> o) \<Rightarrow> i"  (binder "THE " 10)
-  where the_def: "The(P)    == \<Union>({y . x \<in> {0}, P(y)})"
-
-definition If :: "[o, i, i] \<Rightarrow> i"  ("(if (_)/ then (_)/ else (_))" [10] 10)
-  where if_def: "if P then a else b == THE z. P & z=a | ~P & z=b"
-
-abbreviation (input)
-  old_if :: "[o, i, i] => i"  ("if '(_,_,_')")
-  where "if(P,a,b) == If(P,a,b)"
-
-
-subsection \<open>Ordered Pairing\<close>
-
-(* this "symmetric" definition works better than {{a}, {a,b}} *)
-definition Pair :: "[i, i] => i"
-  where "Pair(a,b) == {{a,a}, {a,b}}"
-
-definition fst :: "i \<Rightarrow> i"
-  where "fst(p) == THE a. \<exists>b. p = Pair(a, b)"
-
-definition snd :: "i \<Rightarrow> i"
-  where "snd(p) == THE b. \<exists>a. p = Pair(a, b)"
+lemma iterates_triv:
+     "[| n\<in>nat;  F(x) = x |] ==> F^n (x) = x"
+by (induct n rule: nat_induct, simp_all)
 
-definition split :: "[[i, i] \<Rightarrow> 'a, i] \<Rightarrow> 'a::{}"  \<comment> \<open>for pattern-matching\<close>
-  where "split(c) == \<lambda>p. c(fst(p), snd(p))"
-
-(* Patterns -- extends pre-defined type "pttrn" used in abstractions *)
-nonterminal patterns
-syntax
-  "_pattern"  :: "patterns => pttrn"         ("\<langle>_\<rangle>")
-  ""          :: "pttrn => patterns"         ("_")
-  "_patterns" :: "[pttrn, patterns] => patterns"  ("_,/_")
-  "_Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")
-translations
-  "\<langle>x, y, z\<rangle>"   == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
-  "\<langle>x, y\<rangle>"      == "CONST Pair(x, y)"
-  "\<lambda>\<langle>x,y,zs\<rangle>.b" == "CONST split(\<lambda>x \<langle>y,zs\<rangle>.b)"
-  "\<lambda>\<langle>x,y\<rangle>.b"    == "CONST split(\<lambda>x y. b)"
-
-definition Sigma :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
-  where "Sigma(A,B) == \<Union>x\<in>A. \<Union>y\<in>B(x). {\<langle>x,y\<rangle>}"
-
-abbreviation cart_prod :: "[i, i] => i"  (infixr "\<times>" 80)  \<comment> \<open>Cartesian product\<close>
-  where "A \<times> B \<equiv> Sigma(A, \<lambda>_. B)"
-
-
-subsection \<open>Relations and Functions\<close>
-
-(*converse of relation r, inverse of function*)
-definition converse :: "i \<Rightarrow> i"
-  where "converse(r) == {z. w\<in>r, \<exists>x y. w=\<langle>x,y\<rangle> \<and> z=\<langle>y,x\<rangle>}"
-
-definition domain :: "i \<Rightarrow> i"
-  where "domain(r) == {x. w\<in>r, \<exists>y. w=\<langle>x,y\<rangle>}"
-
-definition range :: "i \<Rightarrow> i"
-  where "range(r) == domain(converse(r))"
-
-definition field :: "i \<Rightarrow> i"
-  where "field(r) == domain(r) \<union> range(r)"
+lemma iterates_type [TC]:
+     "[| n \<in> nat;  a \<in> A; !!x. x \<in> A ==> F(x) \<in> A |]
+      ==> F^n (a) \<in> A"
+by (induct n rule: nat_induct, simp_all)
 
-definition relation :: "i \<Rightarrow> o"  \<comment> \<open>recognizes sets of pairs\<close>
-  where "relation(r) == \<forall>z\<in>r. \<exists>x y. z = \<langle>x,y\<rangle>"
-
-definition "function" :: "i \<Rightarrow> o"  \<comment> \<open>recognizes functions; can have non-pairs\<close>
-  where "function(r) == \<forall>x y. \<langle>x,y\<rangle> \<in> r \<longrightarrow> (\<forall>y'. \<langle>x,y'\<rangle> \<in> r \<longrightarrow> y = y')"
-
-definition Image :: "[i, i] \<Rightarrow> i"  (infixl "``" 90)  \<comment> \<open>image\<close>
-  where image_def: "r `` A  == {y \<in> range(r). \<exists>x\<in>A. \<langle>x,y\<rangle> \<in> r}"
-
-definition vimage :: "[i, i] \<Rightarrow> i"  (infixl "-``" 90)  \<comment> \<open>inverse image\<close>
-  where vimage_def: "r -`` A == converse(r)``A"
-
-(* Restrict the relation r to the domain A *)
-definition restrict :: "[i, i] \<Rightarrow> i"
-  where "restrict(r,A) == {z \<in> r. \<exists>x\<in>A. \<exists>y. z = \<langle>x,y\<rangle>}"
-
-
-(* Abstraction, application and Cartesian product of a family of sets *)
-
-definition Lambda :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
-  where lam_def: "Lambda(A,b) == {\<langle>x,b(x)\<rangle>. x\<in>A}"
-
-definition "apply" :: "[i, i] \<Rightarrow> i"  (infixl "`" 90)  \<comment> \<open>function application\<close>
-  where "f`a == \<Union>(f``{a})"
-
-definition Pi :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
-  where "Pi(A,B) == {f\<in>Pow(Sigma(A,B)). A\<subseteq>domain(f) & function(f)}"
-
-abbreviation function_space :: "[i, i] \<Rightarrow> i"  (infixr "->" 60)  \<comment> \<open>function space\<close>
-  where "A -> B \<equiv> Pi(A, \<lambda>_. B)"
-
-
-(* binder syntax *)
+lemma iterates_omega_triv:
+    "F(x) = x ==> F^\<omega> (x) = x"
+by (simp add: iterates_omega_def iterates_triv)
 
-syntax
-  "_PROD"     :: "[pttrn, i, i] => i"        ("(3\<Prod>_\<in>_./ _)" 10)
-  "_SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sum>_\<in>_./ _)" 10)
-  "_lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
-translations
-  "\<Prod>x\<in>A. B"   == "CONST Pi(A, \<lambda>x. B)"
-  "\<Sum>x\<in>A. B"   == "CONST Sigma(A, \<lambda>x. B)"
-  "\<lambda>x\<in>A. f"    == "CONST Lambda(A, \<lambda>x. f)"
-
-
-subsection \<open>ASCII syntax\<close>
-
-notation (ASCII)
-  cart_prod       (infixr "*" 80) and
-  Int             (infixl "Int" 70) and
-  Un              (infixl "Un" 65) and
-  function_space  (infixr "\<rightarrow>" 60) and
-  Subset          (infixl "<=" 50) and
-  mem             (infixl ":" 50) and
-  not_mem         (infixl "~:" 50)
+lemma Ord_iterates [simp]:
+     "[| n\<in>nat;  !!i. Ord(i) ==> Ord(F(i));  Ord(x) |]
+      ==> Ord(F^n (x))"
+by (induct n rule: nat_induct, simp_all)
 
-syntax (ASCII)
-  "_Ball"     :: "[pttrn, i, o] => o"        ("(3ALL _:_./ _)" 10)
-  "_Bex"      :: "[pttrn, i, o] => o"        ("(3EX _:_./ _)" 10)
-  "_Collect"  :: "[pttrn, i, o] => i"        ("(1{_: _ ./ _})")
-  "_Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})")
-  "_RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _: _})" [51,0,51])
-  "_UNION"    :: "[pttrn, i, i] => i"        ("(3UN _:_./ _)" 10)
-  "_INTER"    :: "[pttrn, i, i] => i"        ("(3INT _:_./ _)" 10)
-  "_PROD"     :: "[pttrn, i, i] => i"        ("(3PROD _:_./ _)" 10)
-  "_SUM"      :: "[pttrn, i, i] => i"        ("(3SUM _:_./ _)" 10)
-  "_lam"      :: "[pttrn, i, i] => i"        ("(3lam _:_./ _)" 10)
-  "_Tuple"    :: "[i, is] => i"              ("<(_,/ _)>")
-  "_pattern"  :: "patterns => pttrn"         ("<_>")
-
-
-subsection \<open>Substitution\<close>
-
-(*Useful examples:  singletonI RS subst_elem,  subst_elem RSN (2,IntI) *)
-lemma subst_elem: "[| b\<in>A;  a=b |] ==> a\<in>A"
-by (erule ssubst, assumption)
+lemma iterates_commute: "n \<in> nat ==> F(F^n (x)) = F^n (F(x))"
+by (induct_tac n, simp_all)
 
 
-subsection\<open>Bounded universal quantifier\<close>
-
-lemma ballI [intro!]: "[| !!x. x\<in>A ==> P(x) |] ==> \<forall>x\<in>A. P(x)"
-by (simp add: Ball_def)
-
-lemmas strip = impI allI ballI
-
-lemma bspec [dest?]: "[| \<forall>x\<in>A. P(x);  x: A |] ==> P(x)"
-by (simp add: Ball_def)
-
-(*Instantiates x first: better for automatic theorem proving?*)
-lemma rev_ballE [elim]:
-    "[| \<forall>x\<in>A. P(x);  x\<notin>A ==> Q;  P(x) ==> Q |] ==> Q"
-by (simp add: Ball_def, blast)
-
-lemma ballE: "[| \<forall>x\<in>A. P(x);  P(x) ==> Q;  x\<notin>A ==> Q |] ==> Q"
-by blast
-
-(*Used in the datatype package*)
-lemma rev_bspec: "[| x: A;  \<forall>x\<in>A. P(x) |] ==> P(x)"
-by (simp add: Ball_def)
-
-(*Trival rewrite rule;   @{term"(\<forall>x\<in>A.P)<->P"} holds only if A is nonempty!*)
-lemma ball_triv [simp]: "(\<forall>x\<in>A. P) <-> ((\<exists>x. x\<in>A) \<longrightarrow> P)"
-by (simp add: Ball_def)
-
-(*Congruence rule for rewriting*)
-lemma ball_cong [cong]:
-    "[| A=A';  !!x. x\<in>A' ==> P(x) <-> P'(x) |] ==> (\<forall>x\<in>A. P(x)) <-> (\<forall>x\<in>A'. P'(x))"
-by (simp add: Ball_def)
-
-lemma atomize_ball:
-    "(!!x. x \<in> A ==> P(x)) == Trueprop (\<forall>x\<in>A. P(x))"
-  by (simp only: Ball_def atomize_all atomize_imp)
-
-lemmas [symmetric, rulify] = atomize_ball
-  and [symmetric, defn] = atomize_ball
-
-
-subsection\<open>Bounded existential quantifier\<close>
+subsection\<open>Transfinite Recursion\<close>
 
-lemma bexI [intro]: "[| P(x);  x: A |] ==> \<exists>x\<in>A. P(x)"
-by (simp add: Bex_def, blast)
-
-(*The best argument order when there is only one @{term"x\<in>A"}*)
-lemma rev_bexI: "[| x\<in>A;  P(x) |] ==> \<exists>x\<in>A. P(x)"
-by blast
-
-(*Not of the general form for such rules. The existential quanitifer becomes universal. *)
-lemma bexCI: "[| \<forall>x\<in>A. ~P(x) ==> P(a);  a: A |] ==> \<exists>x\<in>A. P(x)"
-by blast
-
-lemma bexE [elim!]: "[| \<exists>x\<in>A. P(x);  !!x. [| x\<in>A; P(x) |] ==> Q |] ==> Q"
-by (simp add: Bex_def, blast)
-
-(*We do not even have @{term"(\<exists>x\<in>A. True) <-> True"} unless @{term"A" is nonempty!!*)
-lemma bex_triv [simp]: "(\<exists>x\<in>A. P) <-> ((\<exists>x. x\<in>A) & P)"
-by (simp add: Bex_def)
-
-lemma bex_cong [cong]:
-    "[| A=A';  !!x. x\<in>A' ==> P(x) <-> P'(x) |]
-     ==> (\<exists>x\<in>A. P(x)) <-> (\<exists>x\<in>A'. P'(x))"
-by (simp add: Bex_def cong: conj_cong)
-
-
-
-subsection\<open>Rules for subsets\<close>
-
-lemma subsetI [intro!]:
-    "(!!x. x\<in>A ==> x\<in>B) ==> A \<subseteq> B"
-by (simp add: subset_def)
-
-(*Rule in Modus Ponens style [was called subsetE] *)
-lemma subsetD [elim]: "[| A \<subseteq> B;  c\<in>A |] ==> c\<in>B"
-apply (unfold subset_def)
-apply (erule bspec, assumption)
-done
-
-(*Classical elimination rule*)
-lemma subsetCE [elim]:
-    "[| A \<subseteq> B;  c\<notin>A ==> P;  c\<in>B ==> P |] ==> P"
-by (simp add: subset_def, blast)
+text\<open>Transfinite recursion for definitions based on the
+    three cases of ordinals\<close>
 
-(*Sometimes useful with premises in this order*)
-lemma rev_subsetD: "[| c\<in>A; A<=B |] ==> c\<in>B"
-by blast
-
-lemma contra_subsetD: "[| A \<subseteq> B; c \<notin> B |] ==> c \<notin> A"
-by blast
-
-lemma rev_contra_subsetD: "[| c \<notin> B;  A \<subseteq> B |] ==> c \<notin> A"
-by blast
-
-lemma subset_refl [simp]: "A \<subseteq> A"
-by blast
-
-lemma subset_trans: "[| A<=B;  B<=C |] ==> A<=C"
-by blast
-
-(*Useful for proving A<=B by rewriting in some cases*)
-lemma subset_iff:
-     "A<=B <-> (\<forall>x. x\<in>A \<longrightarrow> x\<in>B)"
-apply (unfold subset_def Ball_def)
-apply (rule iff_refl)
-done
-
-text\<open>For calculations\<close>
-declare subsetD [trans] rev_subsetD [trans] subset_trans [trans]
-
-
-subsection\<open>Rules for equality\<close>
-
-(*Anti-symmetry of the subset relation*)
-lemma equalityI [intro]: "[| A \<subseteq> B;  B \<subseteq> A |] ==> A = B"
-by (rule extension [THEN iffD2], rule conjI)
-
-
-lemma equality_iffI: "(!!x. x\<in>A <-> x\<in>B) ==> A = B"
-by (rule equalityI, blast+)
-
-lemmas equalityD1 = extension [THEN iffD1, THEN conjunct1]
-lemmas equalityD2 = extension [THEN iffD1, THEN conjunct2]
-
-lemma equalityE: "[| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P"
-by (blast dest: equalityD1 equalityD2)
+definition
+  transrec3 :: "[i, i, [i,i]=>i, [i,i]=>i] =>i" where
+    "transrec3(k, a, b, c) ==
+       transrec(k, \<lambda>x r.
+         if x=0 then a
+         else if Limit(x) then c(x, \<lambda>y\<in>x. r`y)
+         else b(Arith.pred(x), r ` Arith.pred(x)))"
 
-lemma equalityCE:
-    "[| A = B;  [| c\<in>A; c\<in>B |] ==> P;  [| c\<notin>A; c\<notin>B |] ==> P |]  ==>  P"
-by (erule equalityE, blast)
-
-lemma equality_iffD:
-  "A = B ==> (!!x. x \<in> A <-> x \<in> B)"
-  by auto
-
-
-subsection\<open>Rules for Replace -- the derived form of replacement\<close>
-
-lemma Replace_iff:
-    "b \<in> {y. x\<in>A, P(x,y)}  <->  (\<exists>x\<in>A. P(x,b) & (\<forall>y. P(x,y) \<longrightarrow> y=b))"
-apply (unfold Replace_def)
-apply (rule replacement [THEN iff_trans], blast+)
-done
+lemma transrec3_0 [simp]: "transrec3(0,a,b,c) = a"
+by (rule transrec3_def [THEN def_transrec, THEN trans], simp)
 
-(*Introduction; there must be a unique y such that P(x,y), namely y=b. *)
-lemma ReplaceI [intro]:
-    "[| P(x,b);  x: A;  !!y. P(x,y) ==> y=b |] ==>
-     b \<in> {y. x\<in>A, P(x,y)}"
-by (rule Replace_iff [THEN iffD2], blast)
-
-(*Elimination; may asssume there is a unique y such that P(x,y), namely y=b. *)
-lemma ReplaceE:
-    "[| b \<in> {y. x\<in>A, P(x,y)};
-        !!x. [| x: A;  P(x,b);  \<forall>y. P(x,y)\<longrightarrow>y=b |] ==> R
-     |] ==> R"
-by (rule Replace_iff [THEN iffD1, THEN bexE], simp+)
+lemma transrec3_succ [simp]:
+     "transrec3(succ(i),a,b,c) = b(i, transrec3(i,a,b,c))"
+by (rule transrec3_def [THEN def_transrec, THEN trans], simp)
 
-(*As above but without the (generally useless) 3rd assumption*)
-lemma ReplaceE2 [elim!]:
-    "[| b \<in> {y. x\<in>A, P(x,y)};
-        !!x. [| x: A;  P(x,b) |] ==> R
-     |] ==> R"
-by (erule ReplaceE, blast)
-
-lemma Replace_cong [cong]:
-    "[| A=B;  !!x y. x\<in>B ==> P(x,y) <-> Q(x,y) |] ==>
-     Replace(A,P) = Replace(B,Q)"
-apply (rule equality_iffI)
-apply (simp add: Replace_iff)
-done
+lemma transrec3_Limit:
+     "Limit(i) ==>
+      transrec3(i,a,b,c) = c(i, \<lambda>j\<in>i. transrec3(j,a,b,c))"
+by (rule transrec3_def [THEN def_transrec, THEN trans], force)
 
 
-subsection\<open>Rules for RepFun\<close>
-
-lemma RepFunI: "a \<in> A ==> f(a) \<in> {f(x). x\<in>A}"
-by (simp add: RepFun_def Replace_iff, blast)
-
-(*Useful for coinduction proofs*)
-lemma RepFun_eqI [intro]: "[| b=f(a);  a \<in> A |] ==> b \<in> {f(x). x\<in>A}"
-apply (erule ssubst)
-apply (erule RepFunI)
-done
-
-lemma RepFunE [elim!]:
-    "[| b \<in> {f(x). x\<in>A};
-        !!x.[| x\<in>A;  b=f(x) |] ==> P |] ==>
-     P"
-by (simp add: RepFun_def Replace_iff, blast)
-
-lemma RepFun_cong [cong]:
-    "[| A=B;  !!x. x\<in>B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)"
-by (simp add: RepFun_def)
-
-lemma RepFun_iff [simp]: "b \<in> {f(x). x\<in>A} <-> (\<exists>x\<in>A. b=f(x))"
-by (unfold Bex_def, blast)
-
-lemma triv_RepFun [simp]: "{x. x\<in>A} = A"
-by blast
-
-
-subsection\<open>Rules for Collect -- forming a subset by separation\<close>
-
-(*Separation is derivable from Replacement*)
-lemma separation [simp]: "a \<in> {x\<in>A. P(x)} <-> a\<in>A & P(a)"
-by (unfold Collect_def, blast)
-
-lemma CollectI [intro!]: "[| a\<in>A;  P(a) |] ==> a \<in> {x\<in>A. P(x)}"
-by simp
-
-lemma CollectE [elim!]: "[| a \<in> {x\<in>A. P(x)};  [| a\<in>A; P(a) |] ==> R |] ==> R"
-by simp
-
-lemma CollectD1: "a \<in> {x\<in>A. P(x)} ==> a\<in>A"
-by (erule CollectE, assumption)
-
-lemma CollectD2: "a \<in> {x\<in>A. P(x)} ==> P(a)"
-by (erule CollectE, assumption)
-
-lemma Collect_cong [cong]:
-    "[| A=B;  !!x. x\<in>B ==> P(x) <-> Q(x) |]
-     ==> Collect(A, %x. P(x)) = Collect(B, %x. Q(x))"
-by (simp add: Collect_def)
-
-
-subsection\<open>Rules for Unions\<close>
-
-declare Union_iff [simp]
-
-(*The order of the premises presupposes that C is rigid; A may be flexible*)
-lemma UnionI [intro]: "[| B: C;  A: B |] ==> A: \<Union>(C)"
-by (simp, blast)
-
-lemma UnionE [elim!]: "[| A \<in> \<Union>(C);  !!B.[| A: B;  B: C |] ==> R |] ==> R"
-by (simp, blast)
-
-
-subsection\<open>Rules for Unions of families\<close>
-(* @{term"\<Union>x\<in>A. B(x)"} abbreviates @{term"\<Union>({B(x). x\<in>A})"} *)
-
-lemma UN_iff [simp]: "b \<in> (\<Union>x\<in>A. B(x)) <-> (\<exists>x\<in>A. b \<in> B(x))"
-by (simp add: Bex_def, blast)
-
-(*The order of the premises presupposes that A is rigid; b may be flexible*)
-lemma UN_I: "[| a: A;  b: B(a) |] ==> b: (\<Union>x\<in>A. B(x))"
-by (simp, blast)
-
-
-lemma UN_E [elim!]:
-    "[| b \<in> (\<Union>x\<in>A. B(x));  !!x.[| x: A;  b: B(x) |] ==> R |] ==> R"
-by blast
-
-lemma UN_cong:
-    "[| A=B;  !!x. x\<in>B ==> C(x)=D(x) |] ==> (\<Union>x\<in>A. C(x)) = (\<Union>x\<in>B. D(x))"
-by simp
-
-
-(*No "Addcongs [UN_cong]" because @{term\<Union>} is a combination of constants*)
-
-(* UN_E appears before UnionE so that it is tried first, to avoid expensive
-  calls to hyp_subst_tac.  Cannot include UN_I as it is unsafe: would enlarge
-  the search space.*)
-
-
-subsection\<open>Rules for the empty set\<close>
-
-(*The set @{term"{x\<in>0. False}"} is empty; by foundation it equals 0
-  See Suppes, page 21.*)
-lemma not_mem_empty [simp]: "a \<notin> 0"
-apply (cut_tac foundation)
-apply (best dest: equalityD2)
-done
-
-lemmas emptyE [elim!] = not_mem_empty [THEN notE]
-
-
-lemma empty_subsetI [simp]: "0 \<subseteq> A"
-by blast
-
-lemma equals0I: "[| !!y. y\<in>A ==> False |] ==> A=0"
-by blast
-
-lemma equals0D [dest]: "A=0 ==> a \<notin> A"
-by blast
-
-declare sym [THEN equals0D, dest]
-
-lemma not_emptyI: "a\<in>A ==> A \<noteq> 0"
-by blast
-
-lemma not_emptyE:  "[| A \<noteq> 0;  !!x. x\<in>A ==> R |] ==> R"
-by blast
-
-
-subsection\<open>Rules for Inter\<close>
-
-(*Not obviously useful for proving InterI, InterD, InterE*)
-lemma Inter_iff: "A \<in> \<Inter>(C) <-> (\<forall>x\<in>C. A: x) & C\<noteq>0"
-by (simp add: Inter_def Ball_def, blast)
-
-(* Intersection is well-behaved only if the family is non-empty! *)
-lemma InterI [intro!]:
-    "[| !!x. x: C ==> A: x;  C\<noteq>0 |] ==> A \<in> \<Inter>(C)"
-by (simp add: Inter_iff)
-
-(*A "destruct" rule -- every B in C contains A as an element, but
-  A\<in>B can hold when B\<in>C does not!  This rule is analogous to "spec". *)
-lemma InterD [elim, Pure.elim]: "[| A \<in> \<Inter>(C);  B \<in> C |] ==> A \<in> B"
-by (unfold Inter_def, blast)
-
-(*"Classical" elimination rule -- does not require exhibiting @{term"B\<in>C"} *)
-lemma InterE [elim]:
-    "[| A \<in> \<Inter>(C);  B\<notin>C ==> R;  A\<in>B ==> R |] ==> R"
-by (simp add: Inter_def, blast)
-
-
-subsection\<open>Rules for Intersections of families\<close>
-
-(* @{term"\<Inter>x\<in>A. B(x)"} abbreviates @{term"\<Inter>({B(x). x\<in>A})"} *)
-
-lemma INT_iff: "b \<in> (\<Inter>x\<in>A. B(x)) <-> (\<forall>x\<in>A. b \<in> B(x)) & A\<noteq>0"
-by (force simp add: Inter_def)
-
-lemma INT_I: "[| !!x. x: A ==> b: B(x);  A\<noteq>0 |] ==> b: (\<Inter>x\<in>A. B(x))"
-by blast
-
-lemma INT_E: "[| b \<in> (\<Inter>x\<in>A. B(x));  a: A |] ==> b \<in> B(a)"
-by blast
-
-lemma INT_cong:
-    "[| A=B;  !!x. x\<in>B ==> C(x)=D(x) |] ==> (\<Inter>x\<in>A. C(x)) = (\<Inter>x\<in>B. D(x))"
-by simp
-
-(*No "Addcongs [INT_cong]" because @{term\<Inter>} is a combination of constants*)
-
-
-subsection\<open>Rules for Powersets\<close>
-
-lemma PowI: "A \<subseteq> B ==> A \<in> Pow(B)"
-by (erule Pow_iff [THEN iffD2])
-
-lemma PowD: "A \<in> Pow(B)  ==>  A<=B"
-by (erule Pow_iff [THEN iffD1])
-
-declare Pow_iff [iff]
-
-lemmas Pow_bottom = empty_subsetI [THEN PowI]    \<comment>\<open>@{term"0 \<in> Pow(B)"}\<close>
-lemmas Pow_top = subset_refl [THEN PowI]         \<comment>\<open>@{term"A \<in> Pow(A)"}\<close>
-
-
-subsection\<open>Cantor's Theorem: There is no surjection from a set to its powerset.\<close>
-
-(*The search is undirected.  Allowing redundant introduction rules may
-  make it diverge.  Variable b represents ANY map, such as
-  (lam x\<in>A.b(x)): A->Pow(A). *)
-lemma cantor: "\<exists>S \<in> Pow(A). \<forall>x\<in>A. b(x) \<noteq> S"
-by (best elim!: equalityCE del: ReplaceI RepFun_eqI)
+declaration \<open>fn _ =>
+  Simplifier.map_ss (Simplifier.set_mksimps (fn ctxt =>
+    map mk_eq o Ord_atomize o Variable.gen_all ctxt))
+\<close>
 
 end
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/ZFC.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ZFC.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -0,0 +1,4 @@
+theory ZFC imports ZF InfDatatype
+begin
+
+end
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/ZF_Base.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/ZF_Base.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -0,0 +1,650 @@
+(*  Title:      ZF/ZF_Base.thy
+    Author:     Lawrence C Paulson and Martin D Coen, CU Computer Laboratory
+    Copyright   1993  University of Cambridge
+*)
+
+section \<open>Base of Zermelo-Fraenkel Set Theory\<close>
+
+theory ZF_Base
+imports "~~/src/FOL/FOL"
+begin
+
+subsection \<open>Signature\<close>
+
+declare [[eta_contract = false]]
+
+typedecl i
+instance i :: "term" ..
+
+axiomatization mem :: "[i, i] \<Rightarrow> o"  (infixl "\<in>" 50)  \<comment> \<open>membership relation\<close>
+  and zero :: "i"  ("0")  \<comment> \<open>the empty set\<close>
+  and Pow :: "i \<Rightarrow> i"  \<comment> \<open>power sets\<close>
+  and Inf :: "i"  \<comment> \<open>infinite set\<close>
+  and Union :: "i \<Rightarrow> i"  ("\<Union>_" [90] 90)
+  and PrimReplace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i"
+
+abbreviation not_mem :: "[i, i] \<Rightarrow> o"  (infixl "\<notin>" 50)  \<comment> \<open>negated membership relation\<close>
+  where "x \<notin> y \<equiv> \<not> (x \<in> y)"
+
+
+subsection \<open>Bounded Quantifiers\<close>
+
+definition Ball :: "[i, i \<Rightarrow> o] \<Rightarrow> o"
+  where "Ball(A, P) \<equiv> \<forall>x. x\<in>A \<longrightarrow> P(x)"
+
+definition Bex :: "[i, i \<Rightarrow> o] \<Rightarrow> o"
+  where "Bex(A, P) \<equiv> \<exists>x. x\<in>A \<and> P(x)"
+
+syntax
+  "_Ball" :: "[pttrn, i, o] \<Rightarrow> o"  ("(3\<forall>_\<in>_./ _)" 10)
+  "_Bex" :: "[pttrn, i, o] \<Rightarrow> o"  ("(3\<exists>_\<in>_./ _)" 10)
+translations
+  "\<forall>x\<in>A. P" \<rightleftharpoons> "CONST Ball(A, \<lambda>x. P)"
+  "\<exists>x\<in>A. P" \<rightleftharpoons> "CONST Bex(A, \<lambda>x. P)"
+
+
+subsection \<open>Variations on Replacement\<close>
+
+(* Derived form of replacement, restricting P to its functional part.
+   The resulting set (for functional P) is the same as with
+   PrimReplace, but the rules are simpler. *)
+definition Replace :: "[i, [i, i] \<Rightarrow> o] \<Rightarrow> i"
+  where "Replace(A,P) == PrimReplace(A, %x y. (\<exists>!z. P(x,z)) & P(x,y))"
+
+syntax
+  "_Replace"  :: "[pttrn, pttrn, i, o] => i"  ("(1{_ ./ _ \<in> _, _})")
+translations
+  "{y. x\<in>A, Q}" \<rightleftharpoons> "CONST Replace(A, \<lambda>x y. Q)"
+
+
+(* Functional form of replacement -- analgous to ML's map functional *)
+
+definition RepFun :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
+  where "RepFun(A,f) == {y . x\<in>A, y=f(x)}"
+
+syntax
+  "_RepFun" :: "[i, pttrn, i] => i"  ("(1{_ ./ _ \<in> _})" [51,0,51])
+translations
+  "{b. x\<in>A}" \<rightleftharpoons> "CONST RepFun(A, \<lambda>x. b)"
+
+
+(* Separation and Pairing can be derived from the Replacement
+   and Powerset Axioms using the following definitions. *)
+definition Collect :: "[i, i \<Rightarrow> o] \<Rightarrow> i"
+  where "Collect(A,P) == {y . x\<in>A, x=y & P(x)}"
+
+syntax
+  "_Collect" :: "[pttrn, i, o] \<Rightarrow> i"  ("(1{_ \<in> _ ./ _})")
+translations
+  "{x\<in>A. P}" \<rightleftharpoons> "CONST Collect(A, \<lambda>x. P)"
+
+
+subsection \<open>General union and intersection\<close>
+
+definition Inter :: "i => i"  ("\<Inter>_" [90] 90)
+  where "\<Inter>(A) == { x\<in>\<Union>(A) . \<forall>y\<in>A. x\<in>y}"
+
+syntax
+  "_UNION" :: "[pttrn, i, i] => i"  ("(3\<Union>_\<in>_./ _)" 10)
+  "_INTER" :: "[pttrn, i, i] => i"  ("(3\<Inter>_\<in>_./ _)" 10)
+translations
+  "\<Union>x\<in>A. B" == "CONST Union({B. x\<in>A})"
+  "\<Inter>x\<in>A. B" == "CONST Inter({B. x\<in>A})"
+
+
+subsection \<open>Finite sets and binary operations\<close>
+
+(*Unordered pairs (Upair) express binary union/intersection and cons;
+  set enumerations translate as {a,...,z} = cons(a,...,cons(z,0)...)*)
+
+definition Upair :: "[i, i] => i"
+  where "Upair(a,b) == {y. x\<in>Pow(Pow(0)), (x=0 & y=a) | (x=Pow(0) & y=b)}"
+
+definition Subset :: "[i, i] \<Rightarrow> o"  (infixl "\<subseteq>" 50)  \<comment> \<open>subset relation\<close>
+  where subset_def: "A \<subseteq> B \<equiv> \<forall>x\<in>A. x\<in>B"
+
+definition Diff :: "[i, i] \<Rightarrow> i"  (infixl "-" 65)  \<comment> \<open>set difference\<close>
+  where "A - B == { x\<in>A . ~(x\<in>B) }"
+
+definition Un :: "[i, i] \<Rightarrow> i"  (infixl "\<union>" 65)  \<comment> \<open>binary union\<close>
+  where "A \<union> B == \<Union>(Upair(A,B))"
+
+definition Int :: "[i, i] \<Rightarrow> i"  (infixl "\<inter>" 70)  \<comment> \<open>binary intersection\<close>
+  where "A \<inter> B == \<Inter>(Upair(A,B))"
+
+definition cons :: "[i, i] => i"
+  where "cons(a,A) == Upair(a,a) \<union> A"
+
+definition succ :: "i => i"
+  where "succ(i) == cons(i, i)"
+
+nonterminal "is"
+syntax
+  "" :: "i \<Rightarrow> is"  ("_")
+  "_Enum" :: "[i, is] \<Rightarrow> is"  ("_,/ _")
+  "_Finset" :: "is \<Rightarrow> i"  ("{(_)}")
+translations
+  "{x, xs}" == "CONST cons(x, {xs})"
+  "{x}" == "CONST cons(x, 0)"
+
+
+subsection \<open>Axioms\<close>
+
+(* ZF axioms -- see Suppes p.238
+   Axioms for Union, Pow and Replace state existence only,
+   uniqueness is derivable using extensionality. *)
+
+axiomatization
+where
+  extension:     "A = B \<longleftrightarrow> A \<subseteq> B \<and> B \<subseteq> A" and
+  Union_iff:     "A \<in> \<Union>(C) \<longleftrightarrow> (\<exists>B\<in>C. A\<in>B)" and
+  Pow_iff:       "A \<in> Pow(B) \<longleftrightarrow> A \<subseteq> B" and
+
+  (*We may name this set, though it is not uniquely defined.*)
+  infinity:      "0 \<in> Inf \<and> (\<forall>y\<in>Inf. succ(y) \<in> Inf)" and
+
+  (*This formulation facilitates case analysis on A.*)
+  foundation:    "A = 0 \<or> (\<exists>x\<in>A. \<forall>y\<in>x. y\<notin>A)" and
+
+  (*Schema axiom since predicate P is a higher-order variable*)
+  replacement:   "(\<forall>x\<in>A. \<forall>y z. P(x,y) \<and> P(x,z) \<longrightarrow> y = z) \<Longrightarrow>
+                         b \<in> PrimReplace(A,P) \<longleftrightarrow> (\<exists>x\<in>A. P(x,b))"
+
+
+subsection \<open>Definite descriptions -- via Replace over the set "1"\<close>
+
+definition The :: "(i \<Rightarrow> o) \<Rightarrow> i"  (binder "THE " 10)
+  where the_def: "The(P)    == \<Union>({y . x \<in> {0}, P(y)})"
+
+definition If :: "[o, i, i] \<Rightarrow> i"  ("(if (_)/ then (_)/ else (_))" [10] 10)
+  where if_def: "if P then a else b == THE z. P & z=a | ~P & z=b"
+
+abbreviation (input)
+  old_if :: "[o, i, i] => i"  ("if '(_,_,_')")
+  where "if(P,a,b) == If(P,a,b)"
+
+
+subsection \<open>Ordered Pairing\<close>
+
+(* this "symmetric" definition works better than {{a}, {a,b}} *)
+definition Pair :: "[i, i] => i"
+  where "Pair(a,b) == {{a,a}, {a,b}}"
+
+definition fst :: "i \<Rightarrow> i"
+  where "fst(p) == THE a. \<exists>b. p = Pair(a, b)"
+
+definition snd :: "i \<Rightarrow> i"
+  where "snd(p) == THE b. \<exists>a. p = Pair(a, b)"
+
+definition split :: "[[i, i] \<Rightarrow> 'a, i] \<Rightarrow> 'a::{}"  \<comment> \<open>for pattern-matching\<close>
+  where "split(c) == \<lambda>p. c(fst(p), snd(p))"
+
+(* Patterns -- extends pre-defined type "pttrn" used in abstractions *)
+nonterminal patterns
+syntax
+  "_pattern"  :: "patterns => pttrn"         ("\<langle>_\<rangle>")
+  ""          :: "pttrn => patterns"         ("_")
+  "_patterns" :: "[pttrn, patterns] => patterns"  ("_,/_")
+  "_Tuple"    :: "[i, is] => i"              ("\<langle>(_,/ _)\<rangle>")
+translations
+  "\<langle>x, y, z\<rangle>"   == "\<langle>x, \<langle>y, z\<rangle>\<rangle>"
+  "\<langle>x, y\<rangle>"      == "CONST Pair(x, y)"
+  "\<lambda>\<langle>x,y,zs\<rangle>.b" == "CONST split(\<lambda>x \<langle>y,zs\<rangle>.b)"
+  "\<lambda>\<langle>x,y\<rangle>.b"    == "CONST split(\<lambda>x y. b)"
+
+definition Sigma :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
+  where "Sigma(A,B) == \<Union>x\<in>A. \<Union>y\<in>B(x). {\<langle>x,y\<rangle>}"
+
+abbreviation cart_prod :: "[i, i] => i"  (infixr "\<times>" 80)  \<comment> \<open>Cartesian product\<close>
+  where "A \<times> B \<equiv> Sigma(A, \<lambda>_. B)"
+
+
+subsection \<open>Relations and Functions\<close>
+
+(*converse of relation r, inverse of function*)
+definition converse :: "i \<Rightarrow> i"
+  where "converse(r) == {z. w\<in>r, \<exists>x y. w=\<langle>x,y\<rangle> \<and> z=\<langle>y,x\<rangle>}"
+
+definition domain :: "i \<Rightarrow> i"
+  where "domain(r) == {x. w\<in>r, \<exists>y. w=\<langle>x,y\<rangle>}"
+
+definition range :: "i \<Rightarrow> i"
+  where "range(r) == domain(converse(r))"
+
+definition field :: "i \<Rightarrow> i"
+  where "field(r) == domain(r) \<union> range(r)"
+
+definition relation :: "i \<Rightarrow> o"  \<comment> \<open>recognizes sets of pairs\<close>
+  where "relation(r) == \<forall>z\<in>r. \<exists>x y. z = \<langle>x,y\<rangle>"
+
+definition "function" :: "i \<Rightarrow> o"  \<comment> \<open>recognizes functions; can have non-pairs\<close>
+  where "function(r) == \<forall>x y. \<langle>x,y\<rangle> \<in> r \<longrightarrow> (\<forall>y'. \<langle>x,y'\<rangle> \<in> r \<longrightarrow> y = y')"
+
+definition Image :: "[i, i] \<Rightarrow> i"  (infixl "``" 90)  \<comment> \<open>image\<close>
+  where image_def: "r `` A  == {y \<in> range(r). \<exists>x\<in>A. \<langle>x,y\<rangle> \<in> r}"
+
+definition vimage :: "[i, i] \<Rightarrow> i"  (infixl "-``" 90)  \<comment> \<open>inverse image\<close>
+  where vimage_def: "r -`` A == converse(r)``A"
+
+(* Restrict the relation r to the domain A *)
+definition restrict :: "[i, i] \<Rightarrow> i"
+  where "restrict(r,A) == {z \<in> r. \<exists>x\<in>A. \<exists>y. z = \<langle>x,y\<rangle>}"
+
+
+(* Abstraction, application and Cartesian product of a family of sets *)
+
+definition Lambda :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
+  where lam_def: "Lambda(A,b) == {\<langle>x,b(x)\<rangle>. x\<in>A}"
+
+definition "apply" :: "[i, i] \<Rightarrow> i"  (infixl "`" 90)  \<comment> \<open>function application\<close>
+  where "f`a == \<Union>(f``{a})"
+
+definition Pi :: "[i, i \<Rightarrow> i] \<Rightarrow> i"
+  where "Pi(A,B) == {f\<in>Pow(Sigma(A,B)). A\<subseteq>domain(f) & function(f)}"
+
+abbreviation function_space :: "[i, i] \<Rightarrow> i"  (infixr "->" 60)  \<comment> \<open>function space\<close>
+  where "A -> B \<equiv> Pi(A, \<lambda>_. B)"
+
+
+(* binder syntax *)
+
+syntax
+  "_PROD"     :: "[pttrn, i, i] => i"        ("(3\<Prod>_\<in>_./ _)" 10)
+  "_SUM"      :: "[pttrn, i, i] => i"        ("(3\<Sum>_\<in>_./ _)" 10)
+  "_lam"      :: "[pttrn, i, i] => i"        ("(3\<lambda>_\<in>_./ _)" 10)
+translations
+  "\<Prod>x\<in>A. B"   == "CONST Pi(A, \<lambda>x. B)"
+  "\<Sum>x\<in>A. B"   == "CONST Sigma(A, \<lambda>x. B)"
+  "\<lambda>x\<in>A. f"    == "CONST Lambda(A, \<lambda>x. f)"
+
+
+subsection \<open>ASCII syntax\<close>
+
+notation (ASCII)
+  cart_prod       (infixr "*" 80) and
+  Int             (infixl "Int" 70) and
+  Un              (infixl "Un" 65) and
+  function_space  (infixr "\<rightarrow>" 60) and
+  Subset          (infixl "<=" 50) and
+  mem             (infixl ":" 50) and
+  not_mem         (infixl "~:" 50)
+
+syntax (ASCII)
+  "_Ball"     :: "[pttrn, i, o] => o"        ("(3ALL _:_./ _)" 10)
+  "_Bex"      :: "[pttrn, i, o] => o"        ("(3EX _:_./ _)" 10)
+  "_Collect"  :: "[pttrn, i, o] => i"        ("(1{_: _ ./ _})")
+  "_Replace"  :: "[pttrn, pttrn, i, o] => i" ("(1{_ ./ _: _, _})")
+  "_RepFun"   :: "[i, pttrn, i] => i"        ("(1{_ ./ _: _})" [51,0,51])
+  "_UNION"    :: "[pttrn, i, i] => i"        ("(3UN _:_./ _)" 10)
+  "_INTER"    :: "[pttrn, i, i] => i"        ("(3INT _:_./ _)" 10)
+  "_PROD"     :: "[pttrn, i, i] => i"        ("(3PROD _:_./ _)" 10)
+  "_SUM"      :: "[pttrn, i, i] => i"        ("(3SUM _:_./ _)" 10)
+  "_lam"      :: "[pttrn, i, i] => i"        ("(3lam _:_./ _)" 10)
+  "_Tuple"    :: "[i, is] => i"              ("<(_,/ _)>")
+  "_pattern"  :: "patterns => pttrn"         ("<_>")
+
+
+subsection \<open>Substitution\<close>
+
+(*Useful examples:  singletonI RS subst_elem,  subst_elem RSN (2,IntI) *)
+lemma subst_elem: "[| b\<in>A;  a=b |] ==> a\<in>A"
+by (erule ssubst, assumption)
+
+
+subsection\<open>Bounded universal quantifier\<close>
+
+lemma ballI [intro!]: "[| !!x. x\<in>A ==> P(x) |] ==> \<forall>x\<in>A. P(x)"
+by (simp add: Ball_def)
+
+lemmas strip = impI allI ballI
+
+lemma bspec [dest?]: "[| \<forall>x\<in>A. P(x);  x: A |] ==> P(x)"
+by (simp add: Ball_def)
+
+(*Instantiates x first: better for automatic theorem proving?*)
+lemma rev_ballE [elim]:
+    "[| \<forall>x\<in>A. P(x);  x\<notin>A ==> Q;  P(x) ==> Q |] ==> Q"
+by (simp add: Ball_def, blast)
+
+lemma ballE: "[| \<forall>x\<in>A. P(x);  P(x) ==> Q;  x\<notin>A ==> Q |] ==> Q"
+by blast
+
+(*Used in the datatype package*)
+lemma rev_bspec: "[| x: A;  \<forall>x\<in>A. P(x) |] ==> P(x)"
+by (simp add: Ball_def)
+
+(*Trival rewrite rule;   @{term"(\<forall>x\<in>A.P)<->P"} holds only if A is nonempty!*)
+lemma ball_triv [simp]: "(\<forall>x\<in>A. P) <-> ((\<exists>x. x\<in>A) \<longrightarrow> P)"
+by (simp add: Ball_def)
+
+(*Congruence rule for rewriting*)
+lemma ball_cong [cong]:
+    "[| A=A';  !!x. x\<in>A' ==> P(x) <-> P'(x) |] ==> (\<forall>x\<in>A. P(x)) <-> (\<forall>x\<in>A'. P'(x))"
+by (simp add: Ball_def)
+
+lemma atomize_ball:
+    "(!!x. x \<in> A ==> P(x)) == Trueprop (\<forall>x\<in>A. P(x))"
+  by (simp only: Ball_def atomize_all atomize_imp)
+
+lemmas [symmetric, rulify] = atomize_ball
+  and [symmetric, defn] = atomize_ball
+
+
+subsection\<open>Bounded existential quantifier\<close>
+
+lemma bexI [intro]: "[| P(x);  x: A |] ==> \<exists>x\<in>A. P(x)"
+by (simp add: Bex_def, blast)
+
+(*The best argument order when there is only one @{term"x\<in>A"}*)
+lemma rev_bexI: "[| x\<in>A;  P(x) |] ==> \<exists>x\<in>A. P(x)"
+by blast
+
+(*Not of the general form for such rules. The existential quanitifer becomes universal. *)
+lemma bexCI: "[| \<forall>x\<in>A. ~P(x) ==> P(a);  a: A |] ==> \<exists>x\<in>A. P(x)"
+by blast
+
+lemma bexE [elim!]: "[| \<exists>x\<in>A. P(x);  !!x. [| x\<in>A; P(x) |] ==> Q |] ==> Q"
+by (simp add: Bex_def, blast)
+
+(*We do not even have @{term"(\<exists>x\<in>A. True) <-> True"} unless @{term"A" is nonempty!!*)
+lemma bex_triv [simp]: "(\<exists>x\<in>A. P) <-> ((\<exists>x. x\<in>A) & P)"
+by (simp add: Bex_def)
+
+lemma bex_cong [cong]:
+    "[| A=A';  !!x. x\<in>A' ==> P(x) <-> P'(x) |]
+     ==> (\<exists>x\<in>A. P(x)) <-> (\<exists>x\<in>A'. P'(x))"
+by (simp add: Bex_def cong: conj_cong)
+
+
+
+subsection\<open>Rules for subsets\<close>
+
+lemma subsetI [intro!]:
+    "(!!x. x\<in>A ==> x\<in>B) ==> A \<subseteq> B"
+by (simp add: subset_def)
+
+(*Rule in Modus Ponens style [was called subsetE] *)
+lemma subsetD [elim]: "[| A \<subseteq> B;  c\<in>A |] ==> c\<in>B"
+apply (unfold subset_def)
+apply (erule bspec, assumption)
+done
+
+(*Classical elimination rule*)
+lemma subsetCE [elim]:
+    "[| A \<subseteq> B;  c\<notin>A ==> P;  c\<in>B ==> P |] ==> P"
+by (simp add: subset_def, blast)
+
+(*Sometimes useful with premises in this order*)
+lemma rev_subsetD: "[| c\<in>A; A<=B |] ==> c\<in>B"
+by blast
+
+lemma contra_subsetD: "[| A \<subseteq> B; c \<notin> B |] ==> c \<notin> A"
+by blast
+
+lemma rev_contra_subsetD: "[| c \<notin> B;  A \<subseteq> B |] ==> c \<notin> A"
+by blast
+
+lemma subset_refl [simp]: "A \<subseteq> A"
+by blast
+
+lemma subset_trans: "[| A<=B;  B<=C |] ==> A<=C"
+by blast
+
+(*Useful for proving A<=B by rewriting in some cases*)
+lemma subset_iff:
+     "A<=B <-> (\<forall>x. x\<in>A \<longrightarrow> x\<in>B)"
+apply (unfold subset_def Ball_def)
+apply (rule iff_refl)
+done
+
+text\<open>For calculations\<close>
+declare subsetD [trans] rev_subsetD [trans] subset_trans [trans]
+
+
+subsection\<open>Rules for equality\<close>
+
+(*Anti-symmetry of the subset relation*)
+lemma equalityI [intro]: "[| A \<subseteq> B;  B \<subseteq> A |] ==> A = B"
+by (rule extension [THEN iffD2], rule conjI)
+
+
+lemma equality_iffI: "(!!x. x\<in>A <-> x\<in>B) ==> A = B"
+by (rule equalityI, blast+)
+
+lemmas equalityD1 = extension [THEN iffD1, THEN conjunct1]
+lemmas equalityD2 = extension [THEN iffD1, THEN conjunct2]
+
+lemma equalityE: "[| A = B;  [| A<=B; B<=A |] ==> P |]  ==>  P"
+by (blast dest: equalityD1 equalityD2)
+
+lemma equalityCE:
+    "[| A = B;  [| c\<in>A; c\<in>B |] ==> P;  [| c\<notin>A; c\<notin>B |] ==> P |]  ==>  P"
+by (erule equalityE, blast)
+
+lemma equality_iffD:
+  "A = B ==> (!!x. x \<in> A <-> x \<in> B)"
+  by auto
+
+
+subsection\<open>Rules for Replace -- the derived form of replacement\<close>
+
+lemma Replace_iff:
+    "b \<in> {y. x\<in>A, P(x,y)}  <->  (\<exists>x\<in>A. P(x,b) & (\<forall>y. P(x,y) \<longrightarrow> y=b))"
+apply (unfold Replace_def)
+apply (rule replacement [THEN iff_trans], blast+)
+done
+
+(*Introduction; there must be a unique y such that P(x,y), namely y=b. *)
+lemma ReplaceI [intro]:
+    "[| P(x,b);  x: A;  !!y. P(x,y) ==> y=b |] ==>
+     b \<in> {y. x\<in>A, P(x,y)}"
+by (rule Replace_iff [THEN iffD2], blast)
+
+(*Elimination; may asssume there is a unique y such that P(x,y), namely y=b. *)
+lemma ReplaceE:
+    "[| b \<in> {y. x\<in>A, P(x,y)};
+        !!x. [| x: A;  P(x,b);  \<forall>y. P(x,y)\<longrightarrow>y=b |] ==> R
+     |] ==> R"
+by (rule Replace_iff [THEN iffD1, THEN bexE], simp+)
+
+(*As above but without the (generally useless) 3rd assumption*)
+lemma ReplaceE2 [elim!]:
+    "[| b \<in> {y. x\<in>A, P(x,y)};
+        !!x. [| x: A;  P(x,b) |] ==> R
+     |] ==> R"
+by (erule ReplaceE, blast)
+
+lemma Replace_cong [cong]:
+    "[| A=B;  !!x y. x\<in>B ==> P(x,y) <-> Q(x,y) |] ==>
+     Replace(A,P) = Replace(B,Q)"
+apply (rule equality_iffI)
+apply (simp add: Replace_iff)
+done
+
+
+subsection\<open>Rules for RepFun\<close>
+
+lemma RepFunI: "a \<in> A ==> f(a) \<in> {f(x). x\<in>A}"
+by (simp add: RepFun_def Replace_iff, blast)
+
+(*Useful for coinduction proofs*)
+lemma RepFun_eqI [intro]: "[| b=f(a);  a \<in> A |] ==> b \<in> {f(x). x\<in>A}"
+apply (erule ssubst)
+apply (erule RepFunI)
+done
+
+lemma RepFunE [elim!]:
+    "[| b \<in> {f(x). x\<in>A};
+        !!x.[| x\<in>A;  b=f(x) |] ==> P |] ==>
+     P"
+by (simp add: RepFun_def Replace_iff, blast)
+
+lemma RepFun_cong [cong]:
+    "[| A=B;  !!x. x\<in>B ==> f(x)=g(x) |] ==> RepFun(A,f) = RepFun(B,g)"
+by (simp add: RepFun_def)
+
+lemma RepFun_iff [simp]: "b \<in> {f(x). x\<in>A} <-> (\<exists>x\<in>A. b=f(x))"
+by (unfold Bex_def, blast)
+
+lemma triv_RepFun [simp]: "{x. x\<in>A} = A"
+by blast
+
+
+subsection\<open>Rules for Collect -- forming a subset by separation\<close>
+
+(*Separation is derivable from Replacement*)
+lemma separation [simp]: "a \<in> {x\<in>A. P(x)} <-> a\<in>A & P(a)"
+by (unfold Collect_def, blast)
+
+lemma CollectI [intro!]: "[| a\<in>A;  P(a) |] ==> a \<in> {x\<in>A. P(x)}"
+by simp
+
+lemma CollectE [elim!]: "[| a \<in> {x\<in>A. P(x)};  [| a\<in>A; P(a) |] ==> R |] ==> R"
+by simp
+
+lemma CollectD1: "a \<in> {x\<in>A. P(x)} ==> a\<in>A"
+by (erule CollectE, assumption)
+
+lemma CollectD2: "a \<in> {x\<in>A. P(x)} ==> P(a)"
+by (erule CollectE, assumption)
+
+lemma Collect_cong [cong]:
+    "[| A=B;  !!x. x\<in>B ==> P(x) <-> Q(x) |]
+     ==> Collect(A, %x. P(x)) = Collect(B, %x. Q(x))"
+by (simp add: Collect_def)
+
+
+subsection\<open>Rules for Unions\<close>
+
+declare Union_iff [simp]
+
+(*The order of the premises presupposes that C is rigid; A may be flexible*)
+lemma UnionI [intro]: "[| B: C;  A: B |] ==> A: \<Union>(C)"
+by (simp, blast)
+
+lemma UnionE [elim!]: "[| A \<in> \<Union>(C);  !!B.[| A: B;  B: C |] ==> R |] ==> R"
+by (simp, blast)
+
+
+subsection\<open>Rules for Unions of families\<close>
+(* @{term"\<Union>x\<in>A. B(x)"} abbreviates @{term"\<Union>({B(x). x\<in>A})"} *)
+
+lemma UN_iff [simp]: "b \<in> (\<Union>x\<in>A. B(x)) <-> (\<exists>x\<in>A. b \<in> B(x))"
+by (simp add: Bex_def, blast)
+
+(*The order of the premises presupposes that A is rigid; b may be flexible*)
+lemma UN_I: "[| a: A;  b: B(a) |] ==> b: (\<Union>x\<in>A. B(x))"
+by (simp, blast)
+
+
+lemma UN_E [elim!]:
+    "[| b \<in> (\<Union>x\<in>A. B(x));  !!x.[| x: A;  b: B(x) |] ==> R |] ==> R"
+by blast
+
+lemma UN_cong:
+    "[| A=B;  !!x. x\<in>B ==> C(x)=D(x) |] ==> (\<Union>x\<in>A. C(x)) = (\<Union>x\<in>B. D(x))"
+by simp
+
+
+(*No "Addcongs [UN_cong]" because @{term\<Union>} is a combination of constants*)
+
+(* UN_E appears before UnionE so that it is tried first, to avoid expensive
+  calls to hyp_subst_tac.  Cannot include UN_I as it is unsafe: would enlarge
+  the search space.*)
+
+
+subsection\<open>Rules for the empty set\<close>
+
+(*The set @{term"{x\<in>0. False}"} is empty; by foundation it equals 0
+  See Suppes, page 21.*)
+lemma not_mem_empty [simp]: "a \<notin> 0"
+apply (cut_tac foundation)
+apply (best dest: equalityD2)
+done
+
+lemmas emptyE [elim!] = not_mem_empty [THEN notE]
+
+
+lemma empty_subsetI [simp]: "0 \<subseteq> A"
+by blast
+
+lemma equals0I: "[| !!y. y\<in>A ==> False |] ==> A=0"
+by blast
+
+lemma equals0D [dest]: "A=0 ==> a \<notin> A"
+by blast
+
+declare sym [THEN equals0D, dest]
+
+lemma not_emptyI: "a\<in>A ==> A \<noteq> 0"
+by blast
+
+lemma not_emptyE:  "[| A \<noteq> 0;  !!x. x\<in>A ==> R |] ==> R"
+by blast
+
+
+subsection\<open>Rules for Inter\<close>
+
+(*Not obviously useful for proving InterI, InterD, InterE*)
+lemma Inter_iff: "A \<in> \<Inter>(C) <-> (\<forall>x\<in>C. A: x) & C\<noteq>0"
+by (simp add: Inter_def Ball_def, blast)
+
+(* Intersection is well-behaved only if the family is non-empty! *)
+lemma InterI [intro!]:
+    "[| !!x. x: C ==> A: x;  C\<noteq>0 |] ==> A \<in> \<Inter>(C)"
+by (simp add: Inter_iff)
+
+(*A "destruct" rule -- every B in C contains A as an element, but
+  A\<in>B can hold when B\<in>C does not!  This rule is analogous to "spec". *)
+lemma InterD [elim, Pure.elim]: "[| A \<in> \<Inter>(C);  B \<in> C |] ==> A \<in> B"
+by (unfold Inter_def, blast)
+
+(*"Classical" elimination rule -- does not require exhibiting @{term"B\<in>C"} *)
+lemma InterE [elim]:
+    "[| A \<in> \<Inter>(C);  B\<notin>C ==> R;  A\<in>B ==> R |] ==> R"
+by (simp add: Inter_def, blast)
+
+
+subsection\<open>Rules for Intersections of families\<close>
+
+(* @{term"\<Inter>x\<in>A. B(x)"} abbreviates @{term"\<Inter>({B(x). x\<in>A})"} *)
+
+lemma INT_iff: "b \<in> (\<Inter>x\<in>A. B(x)) <-> (\<forall>x\<in>A. b \<in> B(x)) & A\<noteq>0"
+by (force simp add: Inter_def)
+
+lemma INT_I: "[| !!x. x: A ==> b: B(x);  A\<noteq>0 |] ==> b: (\<Inter>x\<in>A. B(x))"
+by blast
+
+lemma INT_E: "[| b \<in> (\<Inter>x\<in>A. B(x));  a: A |] ==> b \<in> B(a)"
+by blast
+
+lemma INT_cong:
+    "[| A=B;  !!x. x\<in>B ==> C(x)=D(x) |] ==> (\<Inter>x\<in>A. C(x)) = (\<Inter>x\<in>B. D(x))"
+by simp
+
+(*No "Addcongs [INT_cong]" because @{term\<Inter>} is a combination of constants*)
+
+
+subsection\<open>Rules for Powersets\<close>
+
+lemma PowI: "A \<subseteq> B ==> A \<in> Pow(B)"
+by (erule Pow_iff [THEN iffD2])
+
+lemma PowD: "A \<in> Pow(B)  ==>  A<=B"
+by (erule Pow_iff [THEN iffD1])
+
+declare Pow_iff [iff]
+
+lemmas Pow_bottom = empty_subsetI [THEN PowI]    \<comment>\<open>@{term"0 \<in> Pow(B)"}\<close>
+lemmas Pow_top = subset_refl [THEN PowI]         \<comment>\<open>@{term"A \<in> Pow(A)"}\<close>
+
+
+subsection\<open>Cantor's Theorem: There is no surjection from a set to its powerset.\<close>
+
+(*The search is undirected.  Allowing redundant introduction rules may
+  make it diverge.  Variable b represents ANY map, such as
+  (lam x\<in>A.b(x)): A->Pow(A). *)
+lemma cantor: "\<exists>S \<in> Pow(A). \<forall>x\<in>A. b(x) \<noteq> S"
+by (best elim!: equalityCE del: ReplaceI RepFun_eqI)
+
+end
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/ex/BinEx.thy
--- a/src/ZF/ex/BinEx.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/ex/BinEx.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -5,7 +5,7 @@
 Examples of performing binary arithmetic by simplification.
 *)
 
-theory BinEx imports Main begin
+theory BinEx imports ZF begin
 (*All runtimes below are on a 300MHz Pentium*)
 
 lemma "#13  $+  #19 = #32"
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/ex/CoUnit.thy
--- a/src/ZF/ex/CoUnit.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/ex/CoUnit.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -5,7 +5,7 @@
 
 section \<open>Trivial codatatype definitions, one of which goes wrong!\<close>
 
-theory CoUnit imports Main begin
+theory CoUnit imports ZF begin
 
 text \<open>
   See discussion in: L C Paulson.  A Concrete Final Coalgebra Theorem
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/ex/Commutation.thy
--- a/src/ZF/ex/Commutation.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/ex/Commutation.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -5,7 +5,7 @@
 Commutation theory for proving the Church Rosser theorem.
 *)
 
-theory Commutation imports Main begin
+theory Commutation imports ZF begin
 
 definition
   square  :: "[i, i, i, i] => o" where
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/ex/Group.thy
--- a/src/ZF/ex/Group.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/ex/Group.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -2,7 +2,7 @@
 
 section \<open>Groups\<close>
 
-theory Group imports Main begin
+theory Group imports ZF begin
 
 text\<open>Based on work by Clemens Ballarin, Florian Kammueller, L C Paulson and
 Markus Wenzel.\<close>
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/ex/LList.thy
--- a/src/ZF/ex/LList.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/ex/LList.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -13,7 +13,7 @@
 a typing rule for it, based on some notion of "productivity..."
 *)
 
-theory LList imports Main begin
+theory LList imports ZF begin
 
 consts
   llist  :: "i=>i"
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/ex/Limit.thy
--- a/src/ZF/ex/Limit.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/ex/Limit.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -17,7 +17,7 @@
 Laboratory, 1995.
 *)
 
-theory Limit  imports  Main begin
+theory Limit  imports  ZF begin
 
 definition
   rel :: "[i,i,i]=>o"  where
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/ex/NatSum.thy
--- a/src/ZF/ex/NatSum.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/ex/NatSum.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -16,7 +16,7 @@
 *)
 
 
-theory NatSum imports Main begin
+theory NatSum imports ZF begin
 
 consts sum :: "[i=>i, i] => i"
 primrec 
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/ex/Primes.thy
--- a/src/ZF/ex/Primes.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/ex/Primes.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -5,7 +5,7 @@
 
 section\<open>The Divides Relation and Euclid's algorithm for the GCD\<close>
 
-theory Primes imports Main begin
+theory Primes imports ZF begin
 
 definition
   divides :: "[i,i]=>o"              (infixl "dvd" 50)  where
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/ex/Ramsey.thy
--- a/src/ZF/ex/Ramsey.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/ex/Ramsey.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -24,7 +24,7 @@
   | ram i j = ram (i-1) j + ram i (j-1)
 *)
 
-theory Ramsey imports Main begin
+theory Ramsey imports ZF begin
 
 definition
   Symmetric :: "i=>o" where
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/ex/misc.thy
--- a/src/ZF/ex/misc.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/ex/misc.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -7,7 +7,7 @@
 
 section\<open>Miscellaneous ZF Examples\<close>
 
-theory misc imports Main begin
+theory misc imports ZF begin
 
 
 subsection\<open>Various Small Problems\<close>
diff -r f556a7a9080c -r f3cd78ba687c src/ZF/upair.thy
--- a/src/ZF/upair.thy	Tue Apr 11 10:29:25 2017 +0200
+++ b/src/ZF/upair.thy	Wed Apr 12 13:48:07 2017 +0200
@@ -12,7 +12,7 @@
 section\<open>Unordered Pairs\<close>
 
 theory upair
-imports ZF
+imports ZF_Base
 keywords "print_tcset" :: diag
 begin