attempt to re-establish conventions which theories are loaded into the grand unified library theory;
authorhaftmann
Fri Feb 15 11:47:34 2013 +0100 (2013-02-15)
changeset 511616ed12ae3b3e1
parent 51160 599ff65b85e2
child 51162 310b94ed1815
attempt to re-establish conventions which theories are loaded into the grand unified library theory;
four different code generation tests for different code setup constellations;
augment code generation setup where necessary
src/HOL/Codegenerator_Test/Candidates.thy
src/HOL/Codegenerator_Test/Candidates_Pretty.thy
src/HOL/Codegenerator_Test/Generate.thy
src/HOL/Codegenerator_Test/Generate_Binary_Nat.thy
src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
src/HOL/Codegenerator_Test/Generate_Pretty.thy
src/HOL/Codegenerator_Test/Generate_Pretty_Char.thy
src/HOL/Codegenerator_Test/Generate_Target_Nat.thy
src/HOL/Codegenerator_Test/RBT_Set_Test.thy
src/HOL/Library/AList_Mapping.thy
src/HOL/Library/IArray.thy
src/HOL/Library/Library.thy
src/HOL/Library/Mapping.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/RBT_Mapping.thy
src/HOL/ROOT
     1.1 --- a/src/HOL/Codegenerator_Test/Candidates.thy	Fri Feb 15 11:47:33 2013 +0100
     1.2 +++ b/src/HOL/Codegenerator_Test/Candidates.thy	Fri Feb 15 11:47:34 2013 +0100
     1.3 @@ -7,19 +7,19 @@
     1.4  imports
     1.5    Complex_Main
     1.6    "~~/src/HOL/Library/Library"
     1.7 -  "~~/src/HOL/Library/Sublist"
     1.8 +  "~~/src/HOL/Library/Sublist_Order"
     1.9    "~~/src/HOL/Number_Theory/Primes"
    1.10    "~~/src/HOL/ex/Records"
    1.11  begin
    1.12  
    1.13 -inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
    1.14 -    empty: "sublist [] xs"
    1.15 -  | drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
    1.16 -  | take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
    1.17 +inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
    1.18 +where
    1.19 +  empty: "sublist [] xs"
    1.20 +| drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
    1.21 +| take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
    1.22  
    1.23  code_pred sublist .
    1.24  
    1.25 -(*avoid popular infix*)
    1.26 -code_reserved SML upto
    1.27 +code_reserved SML upto -- {* avoid popular infix *}
    1.28  
    1.29  end
     2.1 --- a/src/HOL/Codegenerator_Test/Candidates_Pretty.thy	Fri Feb 15 11:47:33 2013 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,10 +0,0 @@
     2.4 -
     2.5 -(* Author: Florian Haftmann, TU Muenchen *)
     2.6 -
     2.7 -header {* Generating code using pretty literals and natural number literals  *}
     2.8 -
     2.9 -theory Candidates_Pretty
    2.10 -imports Candidates Code_Char Code_Target_Numeral
    2.11 -begin
    2.12 -
    2.13 -end
     3.1 --- a/src/HOL/Codegenerator_Test/Generate.thy	Fri Feb 15 11:47:33 2013 +0100
     3.2 +++ b/src/HOL/Codegenerator_Test/Generate.thy	Fri Feb 15 11:47:34 2013 +0100
     3.3 @@ -4,11 +4,12 @@
     3.4  header {* Pervasive test of code generator *}
     3.5  
     3.6  theory Generate
     3.7 -imports Candidates
     3.8 +imports
     3.9 +  Candidates
    3.10 +  "~~/src/HOL/Library/AList_Mapping"
    3.11 +  "~~/src/HOL/Library/Finite_Lattice"
    3.12  begin
    3.13  
    3.14 -subsection {* Check whether generated code compiles *}
    3.15 -
    3.16  text {*
    3.17    If any of the checks fails, inspect the code generated
    3.18    by a corresponding @{text export_code} command.
    3.19 @@ -17,3 +18,4 @@
    3.20  export_code _ checking SML OCaml? Haskell? Scala
    3.21  
    3.22  end
    3.23 +
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Codegenerator_Test/Generate_Binary_Nat.thy	Fri Feb 15 11:47:34 2013 +0100
     4.3 @@ -0,0 +1,21 @@
     4.4 +
     4.5 +(* Author: Florian Haftmann, TU Muenchen *)
     4.6 +
     4.7 +header {* Pervasive test of code generator *}
     4.8 +
     4.9 +theory Generate_Binary_Nat
    4.10 +imports
    4.11 +  Candidates
    4.12 +  "~~/src/HOL/Library/AList_Mapping"
    4.13 +  "~~/src/HOL/Library/Finite_Lattice"
    4.14 +  "~~/src/HOL/Library/Code_Binary_Nat"
    4.15 +begin
    4.16 +
    4.17 +text {*
    4.18 +  If any of the checks fails, inspect the code generated
    4.19 +  by a corresponding @{text export_code} command.
    4.20 +*}
    4.21 +
    4.22 +export_code _ checking SML OCaml? Haskell? Scala
    4.23 +
    4.24 +end
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Fri Feb 15 11:47:34 2013 +0100
     5.3 @@ -0,0 +1,73 @@
     5.4 +
     5.5 +(* Author: Ondrej Kuncar, TU Muenchen *)
     5.6 +
     5.7 +header {* Pervasive test of code generator *}
     5.8 +
     5.9 +theory Generate_Efficient_Datastructures
    5.10 +imports
    5.11 +  Candidates
    5.12 +  "~~/src/HOL/Library/DAList"
    5.13 +  "~~/src/HOL/Library/RBT_Mapping"
    5.14 +  "~~/src/HOL/Library/RBT_Set"
    5.15 +begin
    5.16 +
    5.17 +(* 
    5.18 +   The following code equations have to be deleted because they use 
    5.19 +   lists to implement sets in the code generetor. 
    5.20 +*)
    5.21 +
    5.22 +lemma [code, code del]:
    5.23 +  "Sup_pred_inst.Sup_pred = Sup_pred_inst.Sup_pred" ..
    5.24 +
    5.25 +lemma [code, code del]:
    5.26 +  "Inf_pred_inst.Inf_pred = Inf_pred_inst.Inf_pred" ..
    5.27 +
    5.28 +lemma [code, code del]:
    5.29 +  "pred_of_set = pred_of_set" ..
    5.30 +
    5.31 +lemma [code, code del]:
    5.32 +  "acc = acc" ..
    5.33 +
    5.34 +lemma [code, code del]:
    5.35 +  "Cardinality.card' = Cardinality.card'" ..
    5.36 +
    5.37 +lemma [code, code del]:
    5.38 +  "Cardinality.finite' = Cardinality.finite'" ..
    5.39 +
    5.40 +lemma [code, code del]:
    5.41 +  "Cardinality.subset' = Cardinality.subset'" ..
    5.42 +
    5.43 +lemma [code, code del]:
    5.44 +  "Cardinality.eq_set = Cardinality.eq_set" ..
    5.45 +
    5.46 +(*
    5.47 +  If the code generation ends with an exception with the following message:
    5.48 +  '"List.set" is not a constructor, on left hand side of equation: ...',
    5.49 +  the code equation in question has to be either deleted (like many others in this file) 
    5.50 +  or implemented for RBT trees.
    5.51 +*)
    5.52 +
    5.53 +export_code _ checking SML OCaml? Haskell?
    5.54 +
    5.55 +(* Extra setup to make Scala happy *)
    5.56 +(* If the compilation fails with an error "ambiguous implicit values",
    5.57 +   read \<section>7.1 in the Code Generation Manual *)
    5.58 +
    5.59 +class ccpo_linorder = ccpo + linorder
    5.60 +
    5.61 +lemma [code]:
    5.62 +  "(Complete_Partial_Order.admissible :: ('a :: ccpo_linorder \<Rightarrow> bool) \<Rightarrow> bool) P = 
    5.63 +    (\<forall>A. Complete_Partial_Order.chain (op \<le>) A \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (Sup A))"
    5.64 +unfolding admissible_def by blast
    5.65 +
    5.66 +lemma [code]:
    5.67 +  "(gfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Sup {u. u \<le> f u}"
    5.68 +unfolding gfp_def by blast
    5.69 +
    5.70 +lemma [code]:
    5.71 +  "(lfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Inf {u. f u \<le> u}"
    5.72 +unfolding lfp_def by blast
    5.73 +
    5.74 +export_code _ checking Scala?
    5.75 +
    5.76 +end
     6.1 --- a/src/HOL/Codegenerator_Test/Generate_Pretty.thy	Fri Feb 15 11:47:33 2013 +0100
     6.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.3 @@ -1,22 +0,0 @@
     6.4 -
     6.5 -(* Author: Florian Haftmann, TU Muenchen *)
     6.6 -
     6.7 -header {* Pervasive test of code generator using pretty literals *}
     6.8 -
     6.9 -theory Generate_Pretty
    6.10 -imports Candidates_Pretty
    6.11 -begin
    6.12 -
    6.13 -lemma [code, code del]: "nat_of_char = nat_of_char" ..
    6.14 -lemma [code, code del]: "char_of_nat = char_of_nat" ..
    6.15 -
    6.16 -subsection {* Check whether generated code compiles *}
    6.17 -
    6.18 -text {*
    6.19 -  If any of the checks fails, inspect the code generated
    6.20 -  by a corresponding @{text export_code} command.
    6.21 -*}
    6.22 -
    6.23 -export_code _ checking SML OCaml? Haskell? Scala
    6.24 -
    6.25 -end
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/HOL/Codegenerator_Test/Generate_Pretty_Char.thy	Fri Feb 15 11:47:34 2013 +0100
     7.3 @@ -0,0 +1,21 @@
     7.4 +
     7.5 +(* Author: Florian Haftmann, TU Muenchen *)
     7.6 +
     7.7 +header {* Pervasive test of code generator *}
     7.8 +
     7.9 +theory Generate_Pretty_Char
    7.10 +imports
    7.11 +  Candidates
    7.12 +  "~~/src/HOL/Library/AList_Mapping"
    7.13 +  "~~/src/HOL/Library/Finite_Lattice"
    7.14 +  "~~/src/HOL/Library/Code_Char"
    7.15 +begin
    7.16 +
    7.17 +text {*
    7.18 +  If any of the checks fails, inspect the code generated
    7.19 +  by a corresponding @{text export_code} command.
    7.20 +*}
    7.21 +
    7.22 +export_code _ checking SML OCaml? Haskell? Scala
    7.23 +
    7.24 +end
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/HOL/Codegenerator_Test/Generate_Target_Nat.thy	Fri Feb 15 11:47:34 2013 +0100
     8.3 @@ -0,0 +1,21 @@
     8.4 +
     8.5 +(* Author: Florian Haftmann, TU Muenchen *)
     8.6 +
     8.7 +header {* Pervasive test of code generator *}
     8.8 +
     8.9 +theory Generate_Target_Nat
    8.10 +imports
    8.11 +  Candidates
    8.12 +  "~~/src/HOL/Library/AList_Mapping"
    8.13 +  "~~/src/HOL/Library/Finite_Lattice"
    8.14 +  "~~/src/HOL/Library/Code_Target_Numeral"
    8.15 +begin
    8.16 +
    8.17 +text {*
    8.18 +  If any of the checks fails, inspect the code generated
    8.19 +  by a corresponding @{text export_code} command.
    8.20 +*}
    8.21 +
    8.22 +export_code _ checking SML OCaml? Haskell? Scala
    8.23 +
    8.24 +end
     9.1 --- a/src/HOL/Codegenerator_Test/RBT_Set_Test.thy	Fri Feb 15 11:47:33 2013 +0100
     9.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.3 @@ -1,70 +0,0 @@
     9.4 -(*  Title:      HOL/Codegenerator_Test/RBT_Set_Test.thy
     9.5 -    Author:     Ondrej Kuncar
     9.6 -*)
     9.7 -
     9.8 -header {* Test of the code generator using an implementation of sets by RBT trees *}
     9.9 -
    9.10 -theory RBT_Set_Test
    9.11 -imports "~~/src/HOL/Library/Library" "~~/src/HOL/Library/RBT_Set"
    9.12 -begin
    9.13 -
    9.14 -(* 
    9.15 -   The following code equations have to be deleted because they use 
    9.16 -   lists to implement sets in the code generetor. 
    9.17 -*)
    9.18 -
    9.19 -lemma [code, code del]:
    9.20 -  "Sup_pred_inst.Sup_pred = Sup_pred_inst.Sup_pred" ..
    9.21 -
    9.22 -lemma [code, code del]:
    9.23 -  "Inf_pred_inst.Inf_pred = Inf_pred_inst.Inf_pred" ..
    9.24 -
    9.25 -lemma [code, code del]:
    9.26 -  "pred_of_set = pred_of_set" ..
    9.27 -
    9.28 -lemma [code, code del]:
    9.29 -  "acc = acc" ..
    9.30 -
    9.31 -lemma [code, code del]:
    9.32 -  "Cardinality.card' = Cardinality.card'" ..
    9.33 -
    9.34 -lemma [code, code del]:
    9.35 -  "Cardinality.finite' = Cardinality.finite'" ..
    9.36 -
    9.37 -lemma [code, code del]:
    9.38 -  "Cardinality.subset' = Cardinality.subset'" ..
    9.39 -
    9.40 -lemma [code, code del]:
    9.41 -  "Cardinality.eq_set = Cardinality.eq_set" ..
    9.42 -
    9.43 -(*
    9.44 -  If the code generation ends with an exception with the following message:
    9.45 -  '"List.set" is not a constructor, on left hand side of equation: ...',
    9.46 -  the code equation in question has to be either deleted (like many others in this file) 
    9.47 -  or implemented for RBT trees.
    9.48 -*)
    9.49 -
    9.50 -export_code _ checking SML OCaml? Haskell?
    9.51 -
    9.52 -(* Extra setup to make Scala happy *)
    9.53 -(* If the compilation fails with an error "ambiguous implicit values",
    9.54 -   read \<section>7.1 in the Code Generation Manual *)
    9.55 -
    9.56 -class ccpo_linorder = ccpo + linorder
    9.57 -
    9.58 -lemma [code]:
    9.59 -  "(Complete_Partial_Order.admissible :: ('a :: ccpo_linorder \<Rightarrow> bool) \<Rightarrow> bool) P = 
    9.60 -    (\<forall>A. Complete_Partial_Order.chain (op \<le>) A \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (Sup A))"
    9.61 -unfolding admissible_def by blast
    9.62 -
    9.63 -lemma [code]:
    9.64 -  "(gfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Sup {u. u \<le> f u}"
    9.65 -unfolding gfp_def by blast
    9.66 -
    9.67 -lemma [code]:
    9.68 -  "(lfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Inf {u. f u \<le> u}"
    9.69 -unfolding lfp_def by blast
    9.70 -
    9.71 -export_code _ checking Scala?
    9.72 -
    9.73 -end
    10.1 --- a/src/HOL/Library/AList_Mapping.thy	Fri Feb 15 11:47:33 2013 +0100
    10.2 +++ b/src/HOL/Library/AList_Mapping.thy	Fri Feb 15 11:47:34 2013 +0100
    10.3 @@ -59,7 +59,7 @@
    10.4  proof -
    10.5    have aux: "\<And>a b xs. (a, b) \<in> set xs \<Longrightarrow> a \<in> fst ` set xs"
    10.6      by (auto simp add: image_def intro!: bexI)
    10.7 -  show ?thesis apply transfer 
    10.8 +  show ?thesis apply transfer
    10.9    by (auto intro!: map_of_eqI) (auto dest!: map_of_eq_dom intro: aux)
   10.10  qed
   10.11  
    11.1 --- a/src/HOL/Library/IArray.thy	Fri Feb 15 11:47:33 2013 +0100
    11.2 +++ b/src/HOL/Library/IArray.thy	Fri Feb 15 11:47:34 2013 +0100
    11.3 @@ -46,6 +46,26 @@
    11.4  code_const IArray
    11.5    (SML "Vector.fromList")
    11.6  
    11.7 +lemma [code]:
    11.8 +"size (as :: 'a iarray) = 0"
    11.9 +by (cases as) simp
   11.10 +
   11.11 +lemma [code]:
   11.12 +"iarray_size f as = Suc (list_size f (IArray.list_of as))"
   11.13 +by (cases as) simp
   11.14 +
   11.15 +lemma [code]:
   11.16 +"iarray_rec f as = f (IArray.list_of as)"
   11.17 +by (cases as) simp
   11.18 +
   11.19 +lemma [code]:
   11.20 +"iarray_case f as = f (IArray.list_of as)"
   11.21 +by (cases as) simp
   11.22 +
   11.23 +lemma [code]:
   11.24 +"HOL.equal as bs \<longleftrightarrow> HOL.equal (IArray.list_of as) (IArray.list_of bs)"
   11.25 +by (cases as, cases bs) (simp add: equal)
   11.26 +
   11.27  primrec tabulate :: "integer \<times> (integer \<Rightarrow> 'a) \<Rightarrow> 'a iarray" where
   11.28  "tabulate (n, f) = IArray (map (f \<circ> integer_of_nat) [0..<nat_of_integer n])"
   11.29  hide_const (open) tabulate
    12.1 --- a/src/HOL/Library/Library.thy	Fri Feb 15 11:47:33 2013 +0100
    12.2 +++ b/src/HOL/Library/Library.thy	Fri Feb 15 11:47:34 2013 +0100
    12.3 @@ -2,7 +2,7 @@
    12.4  theory Library
    12.5  imports
    12.6    Abstract_Rat
    12.7 -  AList_Mapping
    12.8 +  AList
    12.9    BigO
   12.10    Binomial
   12.11    Bit
   12.12 @@ -29,6 +29,7 @@
   12.13    Indicator_Function
   12.14    Infinite_Set
   12.15    Inner_Product
   12.16 +  IArray
   12.17    Lattice_Algebras
   12.18    Lattice_Syntax
   12.19    ListVector
   12.20 @@ -37,7 +38,6 @@
   12.21    Monad_Syntax
   12.22    Multiset
   12.23    Numeral_Type
   12.24 -  Old_Recdef
   12.25    OptionalSugar
   12.26    Option_ord
   12.27    Parallel
   12.28 @@ -56,11 +56,10 @@
   12.29    Quotient_Type
   12.30    Ramsey
   12.31    Reflection
   12.32 -  RBT_Mapping
   12.33 -  (* RBT_Set *) (* FIXME not included because it breaks Codegenerator_Test/Generate*.thy *)
   12.34    Saturated
   12.35    Set_Algebras
   12.36    State_Monad
   12.37 +  Sublist
   12.38    Sum_of_Squares
   12.39    Transitive_Closure_Table
   12.40    Univ_Poly
    13.1 --- a/src/HOL/Library/Mapping.thy	Fri Feb 15 11:47:33 2013 +0100
    13.2 +++ b/src/HOL/Library/Mapping.thy	Fri Feb 15 11:47:34 2013 +0100
    13.3 @@ -34,11 +34,13 @@
    13.4  lift_definition map :: "('c \<Rightarrow> 'a) \<Rightarrow> ('b \<Rightarrow> 'd) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('c, 'd) mapping" is
    13.5    "\<lambda>f g m. (Option.map g \<circ> m \<circ> f)" .
    13.6  
    13.7 +
    13.8  subsection {* Functorial structure *}
    13.9  
   13.10  enriched_type map: map
   13.11    by (transfer, auto simp add: fun_eq_iff Option.map.compositionality Option.map.id)+
   13.12  
   13.13 +
   13.14  subsection {* Derived operations *}
   13.15  
   13.16  definition ordered_keys :: "('a\<Colon>linorder, 'b) mapping \<Rightarrow> 'a list" where
   13.17 @@ -67,6 +69,22 @@
   13.18  definition map_default :: "'a \<Rightarrow> 'b \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
   13.19    "map_default k v f m = map_entry k f (default k v m)" 
   13.20  
   13.21 +instantiation mapping :: (type, type) equal
   13.22 +begin
   13.23 +
   13.24 +definition
   13.25 +  "HOL.equal m1 m2 \<longleftrightarrow> (\<forall>k. lookup m1 k = lookup m2 k)"
   13.26 +
   13.27 +instance proof
   13.28 +qed (unfold equal_mapping_def, transfer, auto)
   13.29 +
   13.30 +end
   13.31 +
   13.32 +lemma [transfer_rule]:
   13.33 +  "fun_rel cr_mapping (fun_rel cr_mapping HOL.iff) HOL.eq HOL.equal"
   13.34 +  by (unfold equal) transfer_prover
   13.35 +
   13.36 +
   13.37  subsection {* Properties *}
   13.38  
   13.39  lemma lookup_update: "lookup (update k v m) k = Some v" 
   13.40 @@ -258,18 +276,8 @@
   13.41  
   13.42  code_datatype empty update
   13.43  
   13.44 -instantiation mapping :: (type, type) equal
   13.45 -begin
   13.46 -
   13.47 -lift_definition equal_mapping :: "('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping \<Rightarrow> bool" is "op=" .
   13.48 -
   13.49 -instance proof
   13.50 -qed(transfer, rule)
   13.51 -
   13.52 -end
   13.53 -
   13.54 -
   13.55  hide_const (open) empty is_empty rep lookup update delete ordered_keys keys size
   13.56    replace default map_entry map_default tabulate bulkload map
   13.57  
   13.58  end
   13.59 +
    14.1 --- a/src/HOL/Library/Multiset.thy	Fri Feb 15 11:47:33 2013 +0100
    14.2 +++ b/src/HOL/Library/Multiset.thy	Fri Feb 15 11:47:34 2013 +0100
    14.3 @@ -5,7 +5,7 @@
    14.4  header {* (Finite) multisets *}
    14.5  
    14.6  theory Multiset
    14.7 -imports Main DAList
    14.8 +imports Main DAList (* FIXME too specific dependency for a generic theory *)
    14.9  begin
   14.10  
   14.11  subsection {* The type of multisets *}
    15.1 --- a/src/HOL/Library/RBT_Mapping.thy	Fri Feb 15 11:47:33 2013 +0100
    15.2 +++ b/src/HOL/Library/RBT_Mapping.thy	Fri Feb 15 11:47:34 2013 +0100
    15.3 @@ -73,7 +73,7 @@
    15.4  
    15.5  lemma equal_Mapping [code]:
    15.6    "HOL.equal (Mapping t1) (Mapping t2) \<longleftrightarrow> entries t1 = entries t2"
    15.7 -by (transfer fixing: t1 t2) (simp add: entries_lookup)
    15.8 +  by (transfer fixing: t1 t2) (simp add: entries_lookup)
    15.9  
   15.10  lemma [code nbe]:
   15.11    "HOL.equal (x :: (_, _) mapping) x \<longleftrightarrow> True"
    16.1 --- a/src/HOL/ROOT	Fri Feb 15 11:47:33 2013 +0100
    16.2 +++ b/src/HOL/ROOT	Fri Feb 15 11:47:34 2013 +0100
    16.3 @@ -20,18 +20,25 @@
    16.4    description {* Classical Higher-order Logic -- batteries included *}
    16.5    theories
    16.6      Library
    16.7 -    Sublist
    16.8 +    (*conflicting type class instantiations*)
    16.9      List_lexord
   16.10      Sublist_Order
   16.11 -    Finite_Lattice
   16.12 -    Code_Char
   16.13      Product_Lexorder
   16.14      Product_Order
   16.15 +    Finite_Lattice
   16.16 +    (*data refinements and dependent applications*)
   16.17 +    AList_Mapping
   16.18 +    Code_Binary_Nat
   16.19 +    Code_Char
   16.20      (* Code_Prolog  FIXME cf. 76965c356d2a *)
   16.21      Code_Real_Approx_By_Float
   16.22      Code_Target_Numeral
   16.23 -    IArray
   16.24 +    DAList
   16.25 +    RBT_Mapping
   16.26 +    RBT_Set
   16.27 +    (*legacy tools*)
   16.28      Refute
   16.29 +    Old_Recdef
   16.30    theories [condition = ISABELLE_FULL_TEST]
   16.31      Sum_of_Squares_Remote
   16.32    files "document/root.bib" "document/root.tex"
   16.33 @@ -148,7 +155,7 @@
   16.34  
   16.35  session "HOL-Codegenerator_Test" in Codegenerator_Test = "HOL-Library" +
   16.36    options [document = false, document_graph = false, browser_info = false]
   16.37 -  theories Generate Generate_Pretty RBT_Set_Test
   16.38 +  theories Generate Generate_Binary_Nat Generate_Target_Nat Generate_Efficient_Datastructures Generate_Pretty_Char
   16.39  
   16.40  session "HOL-Metis_Examples" in Metis_Examples = HOL +
   16.41    description {*