merged
authornipkow
Mon, 10 Feb 2014 21:51:15 +0100
changeset 55376 d44b415ae99e
parent 55374 636a8523876f (diff)
parent 55375 d26d5f988d71 (current diff)
child 55388 bc34c5774f26
merged
--- a/Admin/Release/CHECKLIST	Mon Feb 10 21:50:50 2014 +0100
+++ b/Admin/Release/CHECKLIST	Mon Feb 10 21:51:15 2014 +0100
@@ -25,6 +25,10 @@
 
 - check funny base directory, e.g. "Test 中国";
 
+- check scalable fonts, e.g. src/Doc/ProgProve (NOTE: T1 encoding
+  requires cm-super fonts, which are usually available on MacTeX or
+  Cygwin, but not on Ubuntu/Debian);
+
 - diff NEWS wrt. last official release, which is read-only;
 
 - update https://bitbucket.org/isabelle_project/isabelle-release/wiki/Home
--- a/lib/texinputs/isabelle.sty	Mon Feb 10 21:50:50 2014 +0100
+++ b/lib/texinputs/isabelle.sty	Mon Feb 10 21:51:15 2014 +0100
@@ -197,6 +197,12 @@
 \chardef\isacharbackquoteclose=`\`%
 }
 
+\newcommand{\isabellestyleliteralunderscore}{%
+\isabellestyleliteral%
+\def\isacharunderscore{\textunderscore}%
+\def\isacharunderscorekeyword{\textunderscore}%
+}
+
 \newcommand{\isabellestylesl}{%
 \isabellestyleit%
 \def\isastyle{\small\sl}%
--- a/src/Doc/Codegen/Further.thy	Mon Feb 10 21:50:50 2014 +0100
+++ b/src/Doc/Codegen/Further.thy	Mon Feb 10 21:51:15 2014 +0100
@@ -33,7 +33,7 @@
   rather than function definitions are always curried.
 
   The second aspect affects user-defined adaptations with @{command
-  code_const}.  For regular terms, the @{text Scala} serializer prints
+  code_printing}.  For regular terms, the @{text Scala} serializer prints
   all type arguments explicitly.  For user-defined term adaptations
   this is only possible for adaptations which take no arguments: here
   the type arguments are just appended.  Otherwise they are ignored;
--- a/src/Doc/IsarImplementation/document/root.tex	Mon Feb 10 21:50:50 2014 +0100
+++ b/src/Doc/IsarImplementation/document/root.tex	Mon Feb 10 21:51:15 2014 +0100
@@ -1,4 +1,5 @@
 \documentclass[12pt,a4paper,fleqn]{report}
+\usepackage[T1]{fontenc}
 \usepackage{latexsym,graphicx}
 \usepackage[refpage]{nomencl}
 \usepackage{iman,extra,isar,proof}
--- a/src/Doc/IsarRef/HOL_Specific.thy	Mon Feb 10 21:50:50 2014 +0100
+++ b/src/Doc/IsarRef/HOL_Specific.thy	Mon Feb 10 21:51:15 2014 +0100
@@ -2386,13 +2386,7 @@
     @{command_def (HOL) "code_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def (HOL) "code_reserved"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def (HOL) "code_printing"} & : & @{text "theory \<rightarrow> theory"} \\
-    @{command_def (HOL) "code_const"} & : & @{text "theory \<rightarrow> theory"} \\
-    @{command_def (HOL) "code_type"} & : & @{text "theory \<rightarrow> theory"} \\
-    @{command_def (HOL) "code_class"} & : & @{text "theory \<rightarrow> theory"} \\
-    @{command_def (HOL) "code_instance"} & : & @{text "theory \<rightarrow> theory"} \\
-    @{command_def (HOL) "code_include"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def (HOL) "code_identifier"} & : & @{text "theory \<rightarrow> theory"} \\
-    @{command_def (HOL) "code_modulename"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def (HOL) "code_monad"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def (HOL) "code_reflect"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def (HOL) "code_pred"} & : & @{text "theory \<rightarrow> proof(prove)"}
@@ -2494,34 +2488,12 @@
       | printing_module ) + '|' )
     ;
 
-    @@{command (HOL) code_const} (const + @'and') \<newline>
-      ( ( '(' target ( syntax ? + @'and' ) ')' ) + )
-    ;
-
-    @@{command (HOL) code_type} (typeconstructor + @'and') \<newline>
-      ( ( '(' target ( syntax ? + @'and' ) ')' ) + )
-    ;
-
-    @@{command (HOL) code_class} (class + @'and') \<newline>
-      ( ( '(' target \<newline> ( @{syntax string} ? + @'and' ) ')' ) + )
-    ;
-
-    @@{command (HOL) code_instance} (( typeconstructor '::' class ) + @'and') \<newline>
-      ( ( '(' target ( '-' ? + @'and' ) ')' ) + )
-    ;
-
-    @@{command (HOL) code_include} target ( @{syntax string} ( @{syntax string} | '-') )
-    ;
-
     @@{command (HOL) code_identifier} ( ( symbol_const | symbol_typeconstructor
       | symbol_class | symbol_class_relation | symbol_class_instance
       | symbol_module ) ( '\<rightharpoonup>' | '=>' ) \<newline>
       ( '(' target ')' @{syntax string} ? + @'and' ) + '|' )
     ;
 
-    @@{command (HOL) code_modulename} target ( ( @{syntax string} @{syntax string} ) + )
-    ;
-
     @@{command (HOL) code_monad} const const target
     ;
 
@@ -2629,10 +2601,7 @@
   \item @{command (HOL) "code_printing"} associates a series of symbols
   (constants, type constructors, classes, class relations, instances,
   module names) with target-specific serializations; omitting a serialization
-  deletes an existing serialization.  Legacy variants of this are
-  @{command (HOL) "code_const"}, @{command (HOL) "code_type"},
-  @{command (HOL) "code_class"}, @{command (HOL) "code_instance"},
-  @{command (HOL) "code_include"}.
+  deletes an existing serialization.
 
   \item @{command (HOL) "code_monad"} provides an auxiliary mechanism
   to generate monadic code for Haskell.
@@ -2642,8 +2611,6 @@
   module names) with target-specific hints how these symbols shall be named.
   These hints gain precedence over names for symbols with no hints at all.
   Conflicting hints are subject to name disambiguation.
-  @{command (HOL) "code_modulename"} is a legacy variant for
-  @{command (HOL) "code_identifier"} on module names.
   \emph{Warning:} It is at the discretion
   of the user to ensure that name prefixes of identifiers in compound
   statements like type classes or datatypes are still the same.
--- a/src/Doc/IsarRef/document/root.tex	Mon Feb 10 21:50:50 2014 +0100
+++ b/src/Doc/IsarRef/document/root.tex	Mon Feb 10 21:51:15 2014 +0100
@@ -1,4 +1,5 @@
 \documentclass[12pt,a4paper,fleqn]{report}
+\usepackage[T1]{fontenc}
 \usepackage{amssymb}
 \usepackage{eurosym}
 \usepackage[english]{babel}
--- a/src/Doc/IsarRef/document/style.sty	Mon Feb 10 21:50:50 2014 +0100
+++ b/src/Doc/IsarRef/document/style.sty	Mon Feb 10 21:51:15 2014 +0100
@@ -39,10 +39,10 @@
 
 \parindent 0pt\parskip 0.5ex
 
-\isabellestyle{literal}
+\isabellestyle{literalunderscore}
 
 \newcommand{\isasymdash}{\isatext{\mbox{-}}}
 
 \railtermfont{\isabellestyle{tt}}
-\railnontermfont{\isabellestyle{literal}}
-\railnamefont{\isabellestyle{literal}}
+\railnontermfont{\isabellestyle{literalunderscore}}
+\railnamefont{\isabellestyle{literalunderscore}}
--- a/src/Doc/System/document/root.tex	Mon Feb 10 21:50:50 2014 +0100
+++ b/src/Doc/System/document/root.tex	Mon Feb 10 21:51:15 2014 +0100
@@ -1,4 +1,5 @@
 \documentclass[12pt,a4paper]{report}
+\usepackage[T1]{fontenc}
 \usepackage{supertabular}
 \usepackage{graphicx}
 \usepackage{iman,extra,isar,ttbox}
--- a/src/HOL/Hoare_Parallel/document/root.tex	Mon Feb 10 21:50:50 2014 +0100
+++ b/src/HOL/Hoare_Parallel/document/root.tex	Mon Feb 10 21:51:15 2014 +0100
@@ -1,6 +1,3 @@
-
-% $Id$
-
 \documentclass[11pt,a4paper]{report}
 \usepackage{graphicx}
 \usepackage[english]{babel}
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Feb 10 21:50:50 2014 +0100
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Feb 10 21:51:15 2014 +0100
@@ -575,7 +575,7 @@
 
 text {* Adaption layer *}
 
-code_include Haskell "Heap"
+code_printing code_module "Heap" \<rightharpoonup> (Haskell)
 {*import qualified Control.Monad;
 import qualified Control.Monad.ST;
 import qualified Data.STRef;
@@ -620,7 +620,7 @@
 
 subsubsection {* Scala *}
 
-code_include Scala "Heap"
+code_printing code_module "Heap" \<rightharpoonup> (Scala)
 {*object Heap {
   def bind[A, B](f: Unit => A, g: A => Unit => B): Unit => B = (_: Unit) => g (f ()) ()
 }
--- a/src/HOL/MicroJava/document/root.tex	Mon Feb 10 21:50:50 2014 +0100
+++ b/src/HOL/MicroJava/document/root.tex	Mon Feb 10 21:51:15 2014 +0100
@@ -1,6 +1,3 @@
-% $Id$
-
-%\documentclass[11pt,a4paper]{article}
 \documentclass[11pt,a4paper]{book}
 \usepackage{graphicx,latexsym,isabelle,isabellesym,pdfsetup}
 
--- a/src/HOL/Number_Theory/Cong.thy	Mon Feb 10 21:50:50 2014 +0100
+++ b/src/HOL/Number_Theory/Cong.thy	Mon Feb 10 21:51:15 2014 +0100
@@ -251,10 +251,7 @@
   done
 
 lemma cong_altdef_int: "[(a::int) = b] (mod m) = (m dvd (a - b))"
-  apply (subst cong_eq_diff_cong_0_int)
-  apply (unfold cong_int_def)
-  apply (simp add: dvd_eq_mod_eq_0 [symmetric])
-  done
+  by (metis cong_int_def zmod_eq_dvd_iff)
 
 lemma cong_abs_int: "[(x::int) = y] (mod abs m) = [x = y] (mod m)"
   by (simp add: cong_altdef_int)
@@ -270,18 +267,11 @@
 
 lemma cong_mult_rcancel_int:
     "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
-  apply (subst (1 2) cong_altdef_int)
-  apply (subst left_diff_distrib [symmetric])
-  apply (rule coprime_dvd_mult_iff_int)
-  apply (subst gcd_commute_int, assumption)
-  done
+  by (metis cong_altdef_int left_diff_distrib coprime_dvd_mult_iff_int gcd_int.commute)
 
 lemma cong_mult_rcancel_nat:
-  assumes  "coprime k (m::nat)"
-  shows "[a * k = b * k] (mod m) = [a = b] (mod m)"
-  apply (rule cong_mult_rcancel_int [transferred])
-  using assms apply auto
-  done
+    "coprime k (m::nat) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
+  by (metis cong_mult_rcancel_int [transferred])
 
 lemma cong_mult_lcancel_nat:
     "coprime k (m::nat) \<Longrightarrow> [k * a = k * b ] (mod m) = [a = b] (mod m)"
@@ -295,16 +285,12 @@
 lemma coprime_cong_mult_int:
   "[(a::int) = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n
     \<Longrightarrow> [a = b] (mod m * n)"
-  apply (simp only: cong_altdef_int)
-  apply (erule (2) divides_mult_int)
-  done
+by (metis divides_mult_int cong_altdef_int)
 
 lemma coprime_cong_mult_nat:
   assumes "[(a::nat) = b] (mod m)" and "[a = b] (mod n)" and "coprime m n"
   shows "[a = b] (mod m * n)"
-  apply (rule coprime_cong_mult_int [transferred])
-  using assms apply auto
-  done
+  by (metis assms coprime_cong_mult_int [transferred])
 
 lemma cong_less_imp_eq_nat: "0 \<le> (a::nat) \<Longrightarrow>
     a < m \<Longrightarrow> 0 \<le> b \<Longrightarrow> b < m \<Longrightarrow> [a = b] (mod m) \<Longrightarrow> a = b"
@@ -316,61 +302,46 @@
 
 lemma cong_less_unique_nat:
     "0 < (m::nat) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
-  apply auto
-  apply (rule_tac x = "a mod m" in exI)
-  apply (unfold cong_nat_def, auto)
-  done
+  by (auto simp: cong_nat_def) (metis mod_less_divisor mod_mod_trivial)
 
 lemma cong_less_unique_int:
     "0 < (m::int) \<Longrightarrow> (\<exists>!b. 0 \<le> b \<and> b < m \<and> [a = b] (mod m))"
-  apply auto
-  apply (rule_tac x = "a mod m" in exI)
-  apply (unfold cong_int_def, auto)
-  done
+  by (auto simp: cong_int_def)  (metis mod_mod_trivial pos_mod_conj)
 
 lemma cong_iff_lin_int: "([(a::int) = b] (mod m)) = (\<exists>k. b = a + m * k)"
-  apply (auto simp add: cong_altdef_int dvd_def field_simps)
+  apply (auto simp add: cong_altdef_int dvd_def)
   apply (rule_tac [!] x = "-k" in exI, auto)
   done
 
-lemma cong_iff_lin_nat: "([(a::nat) = b] (mod m)) =
-    (\<exists>k1 k2. b + k1 * m = a + k2 * m)"
-  apply (rule iffI)
-  apply (cases "b <= a")
-  apply (subst (asm) cong_altdef_nat, assumption)
-  apply (unfold dvd_def, auto)
-  apply (rule_tac x = k in exI)
-  apply (rule_tac x = 0 in exI)
-  apply (auto simp add: field_simps)
-  apply (subst (asm) cong_sym_eq_nat)
-  apply (subst (asm) cong_altdef_nat)
-  apply force
-  apply (unfold dvd_def, auto)
-  apply (rule_tac x = 0 in exI)
-  apply (rule_tac x = k in exI)
-  apply (auto simp add: field_simps)
-  apply (unfold cong_nat_def)
-  apply (subgoal_tac "a mod m = (a + k2 * m) mod m")
-  apply (erule ssubst)back
-  apply (erule subst)
-  apply auto
-  done
+lemma cong_iff_lin_nat: 
+   "([(a::nat) = b] (mod m)) \<longleftrightarrow> (\<exists>k1 k2. b + k1 * m = a + k2 * m)" (is "?lhs = ?rhs")
+proof (rule iffI)
+  assume eqm: ?lhs
+  show ?rhs
+  proof (cases "b \<le> a")
+    case True
+    then show ?rhs using eqm
+      by (metis cong_altdef_nat dvd_def le_add_diff_inverse add_0_right mult_0 mult_commute)
+  next
+    case False
+    then show ?rhs using eqm 
+      apply (subst (asm) cong_sym_eq_nat)
+      apply (auto simp: cong_altdef_nat)
+      apply (metis add_0_right add_diff_inverse dvd_div_mult_self less_or_eq_imp_le mult_0)
+      done
+  qed
+next
+  assume ?rhs
+  then show ?lhs
+    by (metis cong_nat_def mod_mult_self2 nat_mult_commute)
+qed
 
 lemma cong_gcd_eq_int: "[(a::int) = b] (mod m) \<Longrightarrow> gcd a m = gcd b m"
-  apply (subst (asm) cong_iff_lin_int, auto)
-  apply (subst add_commute)
-  apply (subst (2) gcd_commute_int)
-  apply (subst mult_commute)
-  apply (subst gcd_add_mult_int)
-  apply (rule gcd_commute_int)
-  done
+  by (metis cong_int_def gcd_red_int)
 
 lemma cong_gcd_eq_nat:
-  assumes "[(a::nat) = b] (mod m)"
-  shows "gcd a m = gcd b m"
-  apply (rule cong_gcd_eq_int [transferred])
-  using assms apply auto
-  done
+    "[(a::nat) = b] (mod m) \<Longrightarrow>gcd a m = gcd b m"
+  by (metis assms cong_gcd_eq_int [transferred])
 
 lemma cong_imp_coprime_nat: "[(a::nat) = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
   by (auto simp add: cong_gcd_eq_nat)
@@ -385,9 +356,7 @@
   by (auto simp add: cong_int_def)
 
 lemma cong_minus_int [iff]: "[(a::int) = b] (mod -m) = [a = b] (mod m)"
-  apply (subst (1 2) cong_altdef_int)
-  apply auto
-  done
+  by (metis cong_iff_lin_int minus_equation_iff mult_minus_left mult_minus_right)
 
 (*
 lemma mod_dvd_mod_int:
@@ -460,18 +429,14 @@
   by (simp add: cong_nat_def mod_mult2_eq  mod_add_left_eq)
 
 lemma neg_cong_int: "([(a::int) = b] (mod m)) = ([-a = -b] (mod m))"
-  apply (simp add: cong_altdef_int)
-  apply (subst dvd_minus_iff [symmetric])
-  apply (simp add: field_simps)
-  done
+  by (metis cong_int_def minus_minus zminus_zmod)
 
 lemma cong_modulus_neg_int: "([(a::int) = b] (mod m)) = ([a = b] (mod -m))"
   by (auto simp add: cong_altdef_int)
 
 lemma mod_mult_cong_int: "(a::int) ~= 0 \<Longrightarrow> b ~= 0
     \<Longrightarrow> [x mod (a * b) = y] (mod a) \<longleftrightarrow> [x = y] (mod a)"
-  apply (cases "b > 0")
-  apply (simp add: cong_int_def mod_mod_cancel mod_add_left_eq)
+  apply (cases "b > 0", simp add: cong_int_def mod_mod_cancel mod_add_left_eq)
   apply (subst (1 2) cong_modulus_neg_int)
   apply (unfold cong_int_def)
   apply (subgoal_tac "a * b = (-a * -b)")
@@ -482,11 +447,8 @@
   done
 
 lemma cong_to_1_nat: "([(a::nat) = 1] (mod n)) \<Longrightarrow> (n dvd (a - 1))"
-  apply (cases "a = 0")
-  apply force
-  apply (subst (asm) cong_altdef_nat)
-  apply auto
-  done
+  apply (cases "a = 0", force)
+  by (metis cong_altdef_nat leI less_one)
 
 lemma cong_0_1_nat': "[(0::nat) = Suc 0] (mod n) = (n = Suc 0)"
   unfolding cong_nat_def by auto
@@ -503,40 +465,20 @@
   apply auto [1]
   apply (drule_tac x = "a - 1" in spec)
   apply force
-  apply (cases "a = 0")
-  apply (metis add_is_0 cong_0_1_nat zero_neq_one)
+  apply (cases "a = 0", simp add: cong_0_1_nat)
   apply (rule iffI)
-  apply (drule cong_to_1_nat)
-  apply (unfold dvd_def)
-  apply auto [1]
-  apply (rule_tac x = k in exI)
-  apply (auto simp add: field_simps) [1]
-  apply (subst cong_altdef_nat)
-  apply (auto simp add: dvd_def)
+  apply (metis cong_to_1_nat dvd_def monoid_mult_class.mult.right_neutral mult_commute mult_eq_if)
+  apply (metis cong_add_lcancel_0_nat cong_mult_self_nat)
   done
 
 lemma cong_le_nat: "(y::nat) <= x \<Longrightarrow> [x = y] (mod n) \<longleftrightarrow> (\<exists>q. x = q * n + y)"
-  apply (subst cong_altdef_nat)
-  apply assumption
-  apply (unfold dvd_def, auto simp add: field_simps)
-  apply (rule_tac x = k in exI)
-  apply auto
-  done
+  by (metis cong_altdef_nat Nat.le_imp_diff_is_add dvd_def nat_mult_commute)
 
 lemma cong_solve_nat: "(a::nat) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
   apply (cases "n = 0")
   apply force
   apply (frule bezout_nat [of a n], auto)
-  apply (rule exI, erule ssubst)
-  apply (rule cong_trans_nat)
-  apply (rule cong_add_nat)
-  apply (subst mult_commute)
-  apply (rule cong_mult_self_nat)
-  prefer 2
-  apply simp
-  apply (rule cong_refl_nat)
-  apply (rule cong_refl_nat)
-  done
+  by (metis cong_add_rcancel_0_nat cong_mult_self_nat mult_commute)
 
 lemma cong_solve_int: "(a::int) \<noteq> 0 \<Longrightarrow> EX x. [a * x = gcd a n] (mod n)"
   apply (cases "n = 0")
@@ -545,18 +487,7 @@
   apply (rule_tac x = "-1" in exI)
   apply auto
   apply (insert bezout_int [of a n], auto)
-  apply (rule exI)
-  apply (erule subst)
-  apply (rule cong_trans_int)
-  prefer 2
-  apply (rule cong_add_int)
-  apply (rule cong_refl_int)
-  apply (rule cong_sym_int)
-  apply (rule cong_mult_self_int)
-  apply simp
-  apply (subst mult_commute)
-  apply (rule cong_refl_int)
-  done
+  by (metis cong_iff_lin_int mult_commute)
 
 lemma cong_solve_dvd_nat:
   assumes a: "(a::nat) \<noteq> 0" and b: "gcd a n dvd d"
@@ -621,56 +552,34 @@
   apply (subst coprime_iff_invertible_nat)
   apply auto
   apply (auto simp add: cong_nat_def)
-  apply (rule_tac x = "x mod m" in exI)
   apply (metis mod_less_divisor mod_mult_right_eq)
   done
 
 lemma coprime_iff_invertible'_int: "m > (0::int) \<Longrightarrow> coprime a m =
     (EX x. 0 <= x & x < m & [a * x = 1] (mod m))"
   apply (subst coprime_iff_invertible_int)
-  apply auto
   apply (auto simp add: cong_int_def)
-  apply (rule_tac x = "x mod m" in exI)
-  apply (auto simp add: mod_mult_right_eq [symmetric])
+  apply (metis mod_mult_right_eq pos_mod_conj)
   done
 
 lemma cong_cong_lcm_nat: "[(x::nat) = y] (mod a) \<Longrightarrow>
     [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
   apply (cases "y \<le> x")
-  apply (auto simp add: cong_altdef_nat lcm_least_nat) [1]
-  apply (rule cong_sym_nat)
-  apply (subst (asm) (1 2) cong_sym_eq_nat)
-  apply (auto simp add: cong_altdef_nat lcm_least_nat)
+  apply (metis cong_altdef_nat lcm_least_nat)
+  apply (metis cong_altdef_nat cong_diff_cong_0'_nat lcm_semilattice_nat.sup.bounded_iff le0 minus_nat.diff_0)
   done
 
 lemma cong_cong_lcm_int: "[(x::int) = y] (mod a) \<Longrightarrow>
     [x = y] (mod b) \<Longrightarrow> [x = y] (mod lcm a b)"
   by (auto simp add: cong_altdef_int lcm_least_int) [1]
 
-lemma cong_cong_coprime_nat: "coprime a b \<Longrightarrow> [(x::nat) = y] (mod a) \<Longrightarrow>
-    [x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
-  apply (frule (1) cong_cong_lcm_nat)
-  back
-  apply (simp add: lcm_nat_def)
-  done
-
-lemma cong_cong_coprime_int: "coprime a b \<Longrightarrow> [(x::int) = y] (mod a) \<Longrightarrow>
-    [x = y] (mod b) \<Longrightarrow> [x = y] (mod a * b)"
-  apply (frule (1) cong_cong_lcm_int)
-  back
-  apply (simp add: lcm_altdef_int cong_abs_int abs_mult [symmetric])
-  done
-
 lemma cong_cong_setprod_coprime_nat [rule_format]: "finite A \<Longrightarrow>
     (ALL i:A. (ALL j:A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))) \<longrightarrow>
     (ALL i:A. [(x::nat) = y] (mod m i)) \<longrightarrow>
       [x = y] (mod (PROD i:A. m i))"
   apply (induct set: finite)
   apply auto
-  apply (rule cong_cong_coprime_nat)
-  apply (subst gcd_commute_nat)
-  apply (rule setprod_coprime_nat)
-  apply auto
+  apply (metis coprime_cong_mult_nat gcd_semilattice_nat.inf_commute setprod_coprime_nat)
   done
 
 lemma cong_cong_setprod_coprime_int [rule_format]: "finite A \<Longrightarrow>
@@ -679,10 +588,7 @@
       [x = y] (mod (PROD i:A. m i))"
   apply (induct set: finite)
   apply auto
-  apply (rule cong_cong_coprime_int)
-  apply (subst gcd_commute_int)
-  apply (rule setprod_coprime_int)
-  apply auto
+  apply (metis coprime_cong_mult_int gcd_int.commute setprod_coprime_int)
   done
 
 lemma binary_chinese_remainder_aux_nat:
@@ -929,10 +835,7 @@
          [x = y] (mod (PROD i:A. m i))"
   apply (induct set: finite)
   apply auto
-  apply (erule (1) coprime_cong_mult_nat)
-  apply (subst gcd_commute_nat)
-  apply (rule setprod_coprime_nat)
-  apply auto
+  apply (metis coprime_cong_mult_nat nat_mult_commute setprod_coprime_nat)
   done
 
 lemma chinese_remainder_unique_nat:
--- a/src/HOL/Number_Theory/Pocklington.thy	Mon Feb 10 21:50:50 2014 +0100
+++ b/src/HOL/Number_Theory/Pocklington.thy	Mon Feb 10 21:51:15 2014 +0100
@@ -668,7 +668,7 @@
 
 subsection{*Prime factorizations*}
 
-text{*FIXME Some overlap with material in UniqueFactorization, class unique_factorization.*}
+(* FIXME some overlap with material in UniqueFactorization, class unique_factorization *)
 
 definition "primefact ps n = (foldr op * ps  1 = n \<and> (\<forall>p\<in> set ps. prime p))"
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Number_Theory/document/root.tex	Mon Feb 10 21:51:15 2014 +0100
@@ -0,0 +1,28 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage{graphicx}
+\usepackage{isabelle,isabellesym}
+\usepackage{pdfsetup}
+
+\urlstyle{rm}
+\isabellestyle{it}
+
+
+\begin{document}
+
+\title{Various results of number theory}
+\maketitle
+
+\tableofcontents
+
+\begin{center}
+  \includegraphics[width=\textwidth,height=\textheight,keepaspectratio]{session_graph}
+\end{center}
+
+\newpage
+
+\parindent 0pt\parskip 0.5ex
+
+\input{session}
+
+\end{document}
+
--- a/src/HOL/ROOT	Mon Feb 10 21:50:50 2014 +0100
+++ b/src/HOL/ROOT	Mon Feb 10 21:51:15 2014 +0100
@@ -184,6 +184,8 @@
   theories
     Pocklington
     Number_Theory
+  files
+    "document/root.tex"
 
 session "HOL-Old_Number_Theory" in Old_Number_Theory = HOL +
   description {*
--- a/src/HOL/ex/document/root.tex	Mon Feb 10 21:50:50 2014 +0100
+++ b/src/HOL/ex/document/root.tex	Mon Feb 10 21:51:15 2014 +0100
@@ -1,6 +1,3 @@
-
-% $Id$
-
 \documentclass[11pt,a4paper]{article}
 \usepackage{isabelle,isabellesym}
 \usepackage[utf8]{inputenc}
--- a/src/Pure/Isar/code.ML	Mon Feb 10 21:50:50 2014 +0100
+++ b/src/Pure/Isar/code.ML	Mon Feb 10 21:51:15 2014 +0100
@@ -727,8 +727,9 @@
   | Abstract of thm * string
 with
 
-fun dummy_thm thy c =
+fun dummy_thm ctxt c =
   let
+    val thy = Proof_Context.theory_of ctxt;
     val raw_ty = devarify (const_typ thy c);
     val (vs, _) = typscheme thy (c, raw_ty);
     val sortargs = case Axclass.class_of_param thy c
@@ -742,11 +743,12 @@
     val chead = build_head thy (c, ty);
   in Thm.weaken chead Drule.dummy_thm end;
 
-fun nothing_cert thy c = Nothing (dummy_thm thy c);
+fun nothing_cert ctxt c = Nothing (dummy_thm ctxt c);
 
-fun cert_of_eqns thy c [] = Equations (dummy_thm thy c, [])
-  | cert_of_eqns thy c raw_eqns = 
+fun cert_of_eqns ctxt c [] = Equations (dummy_thm ctxt c, [])
+  | cert_of_eqns ctxt c raw_eqns = 
       let
+        val thy = Proof_Context.theory_of ctxt;
         val eqns = burrow_fst (canonize_thms thy) raw_eqns;
         val _ = map (assert_eqn thy) eqns;
         val (thms, propers) = split_list eqns;
@@ -900,32 +902,38 @@
       else Conv.all_conv ct;
   in Conv.combination_conv (Conv.arg_conv lhs_conv) conv ct end;
 
-fun rewrite_eqn thy conv ss =
-  let
-    val ctxt = Proof_Context.init_global thy;
-    val rewrite = Conv.fconv_rule (conv (Simplifier.rewrite (put_simpset ss ctxt)));
-  in singleton (Variable.trade (K (map rewrite)) ctxt) end;
+fun rewrite_eqn conv ctxt =
+  singleton (Variable.trade (K (map (Conv.fconv_rule (conv (Simplifier.rewrite ctxt))))) ctxt)
 
-fun cert_of_eqns_preprocess thy functrans ss c =
-  (map o apfst) (Thm.transfer thy)
-  #> perhaps (perhaps_loop (perhaps_apply functrans))
-  #> (map o apfst) (rewrite_eqn thy eqn_conv ss) 
-  #> (map o apfst) (Axclass.unoverload thy)
-  #> cert_of_eqns thy c;
+fun preprocess conv ctxt =
+  let
+    val thy = Proof_Context.theory_of ctxt;
+  in
+    Thm.transfer thy
+    #> rewrite_eqn conv ctxt
+    #> Axclass.unoverload thy
+  end;
+
+fun cert_of_eqns_preprocess ctxt functrans c =
+  perhaps (perhaps_loop (perhaps_apply functrans))
+  #> (map o apfst) (preprocess eqn_conv ctxt)
+  #> cert_of_eqns ctxt c;
 
 fun get_cert thy { functrans, ss } c =
-  case retrieve_raw thy c
-   of Default (eqns, eqns_lazy) => Lazy.force eqns_lazy
-        |> cert_of_eqns_preprocess thy functrans ss c
+  let
+    val ctxt = thy |> Proof_Context.init_global |> put_simpset ss;
+  in
+    case retrieve_raw thy c of
+      Default (_, eqns_lazy) => Lazy.force eqns_lazy
+        |> cert_of_eqns_preprocess ctxt functrans c
     | Eqns eqns => eqns
-        |> cert_of_eqns_preprocess thy functrans ss c
-    | None => nothing_cert thy c
+        |> cert_of_eqns_preprocess ctxt functrans c
+    | None => nothing_cert ctxt c
     | Proj (_, tyco) => cert_of_proj thy c tyco
     | Abstr (abs_thm, tyco) => abs_thm
-        |> Thm.transfer thy
-        |> rewrite_eqn thy Conv.arg_conv ss
-        |> Axclass.unoverload thy
-        |> cert_of_abs thy tyco c;
+       |> preprocess Conv.arg_conv ctxt
+       |> cert_of_abs thy tyco c
+  end;
 
 
 (* cases *)
--- a/src/Tools/Code/code_haskell.ML	Mon Feb 10 21:50:50 2014 +0100
+++ b/src/Tools/Code/code_haskell.ML	Mon Feb 10 21:51:15 2014 +0100
@@ -183,7 +183,7 @@
               :: str "="
               :: (str o deresolve_const) co
               :: print_typ tyvars BR ty
-              :: (if deriving_show tyco then [str "deriving (Read, Show)"] else [])
+              :: (if deriving_show tyco then [str "deriving (Prelude.Read, Prelude.Show)"] else [])
             )
           end
       | print_stmt (Type_Constructor tyco, Code_Thingol.Datatype (vs, co :: cos)) =
@@ -201,7 +201,7 @@
               :: str "="
               :: print_co co
               :: map ((fn p => Pretty.block [str "| ", p]) o print_co) cos
-              @ (if deriving_show tyco then [str "deriving (Read, Show)"] else [])
+              @ (if deriving_show tyco then [str "deriving (Prelude.Read, Prelude.Show)"] else [])
             )
           end
       | print_stmt (Type_Class class, Code_Thingol.Class (v, (classrels, classparams))) =
@@ -227,37 +227,38 @@
       | print_stmt (_, Code_Thingol.Classinst { class, tyco, vs, inst_params, ... }) =
           let
             val tyvars = intro_vars (map fst vs) reserved;
-            fun requires_args classparam = case const_syntax classparam
-             of NONE => NONE
-              | SOME (_, Code_Printer.Plain_printer _) => SOME 0
-              | SOME (k, Code_Printer.Complex_printer _) => SOME k;
             fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
-              case requires_args classparam
-               of NONE => semicolon [
-                      (str o Long_Name.base_name o deresolve_const) classparam,
+              case const_syntax classparam of
+                NONE => semicolon [
+                    (str o Long_Name.base_name o deresolve_const) classparam,
+                    str "=",
+                    print_app tyvars (SOME thm) reserved NOBR (const, [])
+                  ]
+              | SOME (_, Code_Printer.Plain_printer s) => semicolon [
+                    (str o Long_Name.base_name) s,
+                    str "=",
+                    print_app tyvars (SOME thm) reserved NOBR (const, [])
+                  ]
+              | SOME (k, Code_Printer.Complex_printer _) =>
+                  let
+                    val { sym = Constant c, dom, range, ... } = const;
+                    val (vs, rhs) = (apfst o map) fst
+                      (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
+                    val s = if (is_some o const_syntax) c
+                      then NONE else (SOME o Long_Name.base_name o deresolve_const) c;
+                    val vars = reserved
+                      |> intro_vars (map_filter I (s :: vs));
+                    val lhs = IConst { sym = Constant classparam, typargs = [],
+                      dicts = [], dom = dom, range = range, annotate = false } `$$ map IVar vs;
+                      (*dictionaries are not relevant at this late stage,
+                        and these consts never need type annotations for disambiguation *)
+                  in
+                    semicolon [
+                      print_term tyvars (SOME thm) vars NOBR lhs,
                       str "=",
-                      print_app tyvars (SOME thm) reserved NOBR (const, [])
+                      print_term tyvars (SOME thm) vars NOBR rhs
                     ]
-                | SOME k =>
-                    let
-                      val { sym = Constant c, dom, range, ... } = const;
-                      val (vs, rhs) = (apfst o map) fst
-                        (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
-                      val s = if (is_some o const_syntax) c
-                        then NONE else (SOME o Long_Name.base_name o deresolve_const) c;
-                      val vars = reserved
-                        |> intro_vars (map_filter I (s :: vs));
-                      val lhs = IConst { sym = Constant classparam, typargs = [],
-                        dicts = [], dom = dom, range = range, annotate = false } `$$ map IVar vs;
-                        (*dictionaries are not relevant at this late stage,
-                          and these consts never need type annotations for disambiguation *)
-                    in
-                      semicolon [
-                        print_term tyvars (SOME thm) vars NOBR lhs,
-                        str "=",
-                        print_term tyvars (SOME thm) vars NOBR rhs
-                      ]
-                    end;
+                  end;
           in
             Pretty.block_enclose (
               Pretty.block [
--- a/src/Tools/Code/code_preproc.ML	Mon Feb 10 21:50:50 2014 +0100
+++ b/src/Tools/Code/code_preproc.ML	Mon Feb 10 21:51:15 2014 +0100
@@ -264,15 +264,16 @@
 
 (* retrieving equations and instances from the background context *)
 
-fun obtain_eqns thy eqngr c =
+fun obtain_eqns ctxt eqngr c =
   case try (Graph.get_node eqngr) c
    of SOME (lhs, cert) => ((lhs, []), cert)
     | NONE => let
+        val thy = Proof_Context.theory_of ctxt;
         val functrans = (map (fn (_, (_, f)) => f thy)
           o #functrans o the_thmproc) thy;
-        val {pre, ...} = the_thmproc thy;
-        val cert = Code.get_cert thy { functrans = functrans, ss = pre } c;
-        val (lhs, rhss) = Code.typargs_deps_of_cert thy cert;
+        val cert = Code.get_cert thy { functrans = functrans, ss = simpset_of ctxt } c; (*FIXME*)
+        val (lhs, rhss) =
+          Code.typargs_deps_of_cert thy cert;
       in ((lhs, rhss), cert) end;
 
 fun obtain_instance thy arities (inst as (class, tyco)) =
@@ -289,7 +290,7 @@
 
 (* computing instantiations *)
 
-fun add_classes thy arities eqngr c_k new_classes vardeps_data =
+fun add_classes ctxt arities eqngr c_k new_classes vardeps_data =
   let
     val (styps, old_classes) = Vargraph.get_node (fst vardeps_data) c_k;
     val diff_classes = new_classes |> subtract (op =) old_classes;
@@ -299,82 +300,82 @@
   in
     vardeps_data
     |> (apfst o Vargraph.map_node c_k o apsnd) (append diff_classes)
-    |> fold (fn styp => fold (ensure_typmatch_inst thy arities eqngr styp) new_classes) styps
-    |> fold (fn c_k => add_classes thy arities eqngr c_k diff_classes) c_ks
+    |> fold (fn styp => fold (ensure_typmatch_inst ctxt arities eqngr styp) new_classes) styps
+    |> fold (fn c_k => add_classes ctxt arities eqngr c_k diff_classes) c_ks
   end end
-and add_styp thy arities eqngr c_k new_tyco_styps vardeps_data =
+and add_styp ctxt arities eqngr c_k new_tyco_styps vardeps_data =
   let
     val (old_tyco_stypss, classes) = Vargraph.get_node (fst vardeps_data) c_k;
   in if member (op =) old_tyco_stypss new_tyco_styps then vardeps_data
   else
     vardeps_data
     |> (apfst o Vargraph.map_node c_k o apfst) (cons new_tyco_styps)
-    |> fold (ensure_typmatch_inst thy arities eqngr new_tyco_styps) classes
+    |> fold (ensure_typmatch_inst ctxt arities eqngr new_tyco_styps) classes
   end
-and add_dep thy arities eqngr c_k c_k' vardeps_data =
+and add_dep ctxt arities eqngr c_k c_k' vardeps_data =
   let
     val (_, classes) = Vargraph.get_node (fst vardeps_data) c_k;
   in
     vardeps_data
-    |> add_classes thy arities eqngr c_k' classes
+    |> add_classes ctxt arities eqngr c_k' classes
     |> apfst (Vargraph.add_edge (c_k, c_k'))
   end
-and ensure_typmatch_inst thy arities eqngr (tyco, styps) class vardeps_data =
-  if can (Sign.arity_sorts thy tyco) [class]
+and ensure_typmatch_inst ctxt arities eqngr (tyco, styps) class vardeps_data =
+  if can (Sign.arity_sorts (Proof_Context.theory_of ctxt) tyco) [class]
   then vardeps_data
-    |> ensure_inst thy arities eqngr (class, tyco)
+    |> ensure_inst ctxt arities eqngr (class, tyco)
     |> fold_index (fn (k, styp) =>
-         ensure_typmatch thy arities eqngr styp (Inst (class, tyco), k)) styps
+         ensure_typmatch ctxt arities eqngr styp (Inst (class, tyco), k)) styps
   else vardeps_data (*permissive!*)
-and ensure_inst thy arities eqngr (inst as (class, tyco)) (vardeps_data as (_, (_, insts))) =
+and ensure_inst ctxt arities eqngr (inst as (class, tyco)) (vardeps_data as (_, (_, insts))) =
   if member (op =) insts inst then vardeps_data
   else let
     val (classess, (super_classes, inst_params)) =
-      obtain_instance thy arities inst;
+      obtain_instance (Proof_Context.theory_of ctxt) arities inst;
   in
     vardeps_data
     |> (apsnd o apsnd) (insert (op =) inst)
     |> fold_index (fn (k, _) =>
          apfst (Vargraph.new_node ((Inst (class, tyco), k), ([] ,[])))) classess
-    |> fold (fn super_class => ensure_inst thy arities eqngr (super_class, tyco)) super_classes
-    |> fold (ensure_fun thy arities eqngr) inst_params
+    |> fold (fn super_class => ensure_inst ctxt arities eqngr (super_class, tyco)) super_classes
+    |> fold (ensure_fun ctxt arities eqngr) inst_params
     |> fold_index (fn (k, classes) =>
-         add_classes thy arities eqngr (Inst (class, tyco), k) classes
+         add_classes ctxt arities eqngr (Inst (class, tyco), k) classes
          #> fold (fn super_class =>
-             add_dep thy arities eqngr (Inst (super_class, tyco), k)
+             add_dep ctxt arities eqngr (Inst (super_class, tyco), k)
              (Inst (class, tyco), k)) super_classes
          #> fold (fn inst_param =>
-             add_dep thy arities eqngr (Fun inst_param, k)
+             add_dep ctxt arities eqngr (Fun inst_param, k)
              (Inst (class, tyco), k)
              ) inst_params
          ) classess
   end
-and ensure_typmatch thy arities eqngr (Tyco tyco_styps) c_k vardeps_data =
+and ensure_typmatch ctxt arities eqngr (Tyco tyco_styps) c_k vardeps_data =
       vardeps_data
-      |> add_styp thy arities eqngr c_k tyco_styps
-  | ensure_typmatch thy arities eqngr (Var c_k') c_k vardeps_data =
+      |> add_styp ctxt arities eqngr c_k tyco_styps
+  | ensure_typmatch ctxt arities eqngr (Var c_k') c_k vardeps_data =
       vardeps_data
-      |> add_dep thy arities eqngr c_k c_k'
-  | ensure_typmatch thy arities eqngr Free c_k vardeps_data =
+      |> add_dep ctxt arities eqngr c_k c_k'
+  | ensure_typmatch ctxt arities eqngr Free c_k vardeps_data =
       vardeps_data
-and ensure_rhs thy arities eqngr (c', styps) vardeps_data =
+and ensure_rhs ctxt arities eqngr (c', styps) vardeps_data =
   vardeps_data
-  |> ensure_fun thy arities eqngr c'
+  |> ensure_fun ctxt arities eqngr c'
   |> fold_index (fn (k, styp) =>
-       ensure_typmatch thy arities eqngr styp (Fun c', k)) styps
-and ensure_fun thy arities eqngr c (vardeps_data as (_, (eqntab, _))) =
+       ensure_typmatch ctxt arities eqngr styp (Fun c', k)) styps
+and ensure_fun ctxt arities eqngr c (vardeps_data as (_, (eqntab, _))) =
   if Symtab.defined eqntab c then vardeps_data
   else let
-    val ((lhs, rhss), eqns) = obtain_eqns thy eqngr c;
+    val ((lhs, rhss), eqns) = obtain_eqns ctxt eqngr c;
     val rhss' = (map o apsnd o map) (styp_of (SOME (c, lhs))) rhss;
   in
     vardeps_data
     |> (apsnd o apfst) (Symtab.update_new (c, (lhs, eqns)))
     |> fold_index (fn (k, _) =>
          apfst (Vargraph.new_node ((Fun c, k), ([] ,[])))) lhs
-    |> fold_index (fn (k, (_, sort)) =>
-         add_classes thy arities eqngr (Fun c, k) (complete_proper_sort thy sort)) lhs
-    |> fold (ensure_rhs thy arities eqngr) rhss'
+    |> fold_index (fn (k, (_, sort)) => add_classes ctxt arities eqngr (Fun c, k)
+         (complete_proper_sort (Proof_Context.theory_of ctxt) sort)) lhs
+    |> fold (ensure_rhs ctxt arities eqngr) rhss'
   end;
 
 
@@ -413,11 +414,13 @@
 
 fun extend_arities_eqngr thy cs ts (arities, (eqngr : code_graph)) =
   let
+    val {pre, ...} = the_thmproc thy;
+    val ctxt = thy |> Proof_Context.init_global |> put_simpset pre;
     val cs_rhss = (fold o fold_aterms) (fn Const (c_ty as (c, _)) =>
       insert (op =) (c, (map (styp_of NONE) o Sign.const_typargs thy) c_ty) | _ => I) ts [];
     val (vardeps, (eqntab, insts)) = empty_vardeps_data
-      |> fold (ensure_fun thy arities eqngr) cs
-      |> fold (ensure_rhs thy arities eqngr) cs_rhss;
+      |> fold (ensure_fun ctxt arities eqngr) cs
+      |> fold (ensure_rhs ctxt arities eqngr) cs_rhss;
     val arities' = fold (add_arity thy vardeps) insts arities;
     val algebra = Sorts.subalgebra (Context.pretty_global thy) (is_proper_class thy)
       (AList.lookup (op =) arities') (Sign.classes_of thy);
--- a/src/Tools/Code/code_target.ML	Mon Feb 10 21:50:50 2014 +0100
+++ b/src/Tools/Code/code_target.ML	Mon Feb 10 21:51:15 2014 +0100
@@ -53,16 +53,9 @@
   type identifier_data
   val set_identifiers: (string, string, string, string, string, string) symbol_attr_decl
     -> theory -> theory
-  type raw_const_syntax = Code_Printer.raw_const_syntax
-  type tyco_syntax = Code_Printer.tyco_syntax
-  val set_printings: (raw_const_syntax, tyco_syntax, string, unit, unit, (string * string list)) symbol_attr_decl
+  val set_printings: (Code_Printer.raw_const_syntax, Code_Printer.tyco_syntax, string, unit, unit, (string * string list)) symbol_attr_decl
     -> theory -> theory
-  val add_const_syntax: string -> string -> raw_const_syntax option -> theory -> theory
-  val add_tyco_syntax: string -> string -> tyco_syntax option -> theory -> theory
-  val add_class_syntax: string -> class -> string option -> theory -> theory
-  val add_instance_syntax: string -> class * string -> unit option -> theory -> theory
   val add_reserved: string -> string -> theory -> theory
-  val add_include: string -> string * (string * string list) option -> theory -> theory
 
   val codegen_tool: string (*theory name*) -> string (*export_code expr*) -> unit
 
@@ -584,15 +577,6 @@
 val set_identifiers = gen_set_identifiers cert_name_decls;
 val set_identifiers_cmd = gen_set_identifiers read_name_decls;
 
-fun add_module_alias_cmd target aliasses thy =
-  let
-    val _ = legacy_feature "prefer \"code_identifier\" over \"code_modulename\"";
-  in
-    fold (fn (sym, name) => set_identifier
-      (target, Code_Symbol.Module (sym, if name = "" then NONE else SOME (check_name true name))))
-      aliasses thy
-  end;
-
 
 (* custom printings *)
 
@@ -620,62 +604,9 @@
 val set_printings = gen_set_printings cert_printings;
 val set_printings_cmd = gen_set_printings read_printings;
 
-fun gen_add_syntax Symbol prep_x prep_syn target raw_x some_raw_syn thy =
-  let
-    val _ = legacy_feature "prefer \"code_printing\" for custom serialisations"
-    val x = prep_x thy raw_x;
-  in set_printing (target, Symbol (x, Option.map (prep_syn thy target x) some_raw_syn)) thy end;
-
-fun gen_add_const_syntax prep_const =
-  gen_add_syntax Constant prep_const check_const_syntax;
-
-fun gen_add_tyco_syntax prep_tyco =
-  gen_add_syntax Type_Constructor prep_tyco check_tyco_syntax;
-
-fun gen_add_class_syntax prep_class =
-  gen_add_syntax Type_Class prep_class ((K o K o K) I);
-
-fun gen_add_instance_syntax prep_inst =
-  gen_add_syntax Class_Instance prep_inst ((K o K o K) I);
-
-fun gen_add_include prep_const target (name, some_content) thy =
-  gen_add_syntax Module (K I)
-    (fn thy => fn _ => fn _ => fn (raw_content, raw_cs) => (Code_Printer.str raw_content, map (prep_const thy) raw_cs))
-    target name some_content thy;
-
 
 (* concrete syntax *)
 
-local
-
-fun zip_list (x :: xs) f g =
-  f
-  :|-- (fn y =>
-    fold_map (fn x => g |-- f >> pair x) xs
-    :|-- (fn xys => pair ((x, y) :: xys)));
-
-fun process_multi_syntax parse_thing parse_syntax change =
-  (Parse.and_list1 parse_thing
-  :|-- (fn things => Scan.repeat1 (@{keyword "("} |-- Parse.name --
-        (zip_list things (Scan.option parse_syntax) @{keyword "and"}) --| @{keyword ")"})))
-  >> (Toplevel.theory oo fold)
-    (fn (target, syns) => fold (fn (raw_x, syn) => change target raw_x syn) syns);
-
-in
-
-val add_reserved = add_reserved;
-val add_const_syntax = gen_add_const_syntax (K I);
-val add_tyco_syntax = gen_add_tyco_syntax cert_tyco;
-val add_class_syntax = gen_add_class_syntax cert_class;
-val add_instance_syntax = gen_add_instance_syntax cert_inst;
-val add_include = gen_add_include (K I);
-
-val add_const_syntax_cmd = gen_add_const_syntax Code.read_const;
-val add_tyco_syntax_cmd = gen_add_tyco_syntax read_tyco;
-val add_class_syntax_cmd = gen_add_class_syntax read_class;
-val add_instance_syntax_cmd = gen_add_instance_syntax read_inst;
-val add_include_cmd = gen_add_include Code.read_const;
-
 fun parse_args f args =
   case Scan.read Token.stopper f args
    of SOME x => x
@@ -736,11 +667,6 @@
       >> (Toplevel.theory o fold set_identifiers_cmd));
 
 val _ =
-  Outer_Syntax.command @{command_spec "code_modulename"} "alias module to other name"
-    (Parse.name -- Scan.repeat1 (Parse.name -- Parse.name)
-      >> (fn (target, modlnames) => (Toplevel.theory o add_module_alias_cmd target) modlnames));
-
-val _ =
   Outer_Syntax.command @{command_spec "code_printing"} "declare dedicated printing for code symbols"
     (parse_symbol_pragmas (Code_Printer.parse_const_syntax) (Code_Printer.parse_tyco_syntax)
       Parse.string (Parse.minus >> K ()) (Parse.minus >> K ())
@@ -748,40 +674,9 @@
       >> (Toplevel.theory o fold set_printings_cmd));
 
 val _ =
-  Outer_Syntax.command @{command_spec "code_const"} "define code syntax for constant"
-    (process_multi_syntax Parse.term Code_Printer.parse_const_syntax
-      add_const_syntax_cmd);
-
-val _ =
-  Outer_Syntax.command @{command_spec "code_type"} "define code syntax for type constructor"
-    (process_multi_syntax Parse.type_const Code_Printer.parse_tyco_syntax
-      add_tyco_syntax_cmd);
-
-val _ =
-  Outer_Syntax.command @{command_spec "code_class"} "define code syntax for class"
-    (process_multi_syntax Parse.class Parse.string
-      add_class_syntax_cmd);
-
-val _ =
-  Outer_Syntax.command @{command_spec "code_instance"} "define code syntax for instance"
-    (process_multi_syntax parse_inst_ident (Parse.minus >> K ())
-      add_instance_syntax_cmd);
-
-val _ =
-  Outer_Syntax.command @{command_spec "code_include"}
-    "declare piece of code to be included in generated code"
-    (Parse.name -- Parse.name -- (Parse.text :|--
-      (fn "-" => Scan.succeed NONE
-        | s => Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term) [] >> pair s >> SOME))
-      >> (fn ((target, name), content_consts) =>
-          (Toplevel.theory o add_include_cmd target) (name, content_consts)));
-
-val _ =
   Outer_Syntax.command @{command_spec "export_code"} "generate executable code for constants"
     (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
 
-end; (*local*)
-
 
 (** external entrance point -- for codegen tool **)
 
--- a/src/Tools/Code_Generator.thy	Mon Feb 10 21:50:50 2014 +0100
+++ b/src/Tools/Code_Generator.thy	Mon Feb 10 21:51:15 2014 +0100
@@ -8,8 +8,7 @@
 imports Pure
 keywords
   "value" "print_codeproc" "code_thms" "code_deps" :: diag and
-  "export_code" "code_identifier" "code_printing" "code_class" "code_instance" "code_type"
-    "code_const" "code_reserved" "code_include" "code_modulename"
+  "export_code" "code_identifier" "code_printing" "code_reserved"
     "code_monad" "code_reflect" :: thy_decl and
   "datatypes" "functions" "module_name" "file" "checking"
   "constant" "type_constructor" "type_class" "class_relation" "class_instance" "code_module"