isabelle: src/HOL/Library/ROOT.ML@c05e8209a3aa (annotated)

37694 19e8b730ddeb tuned bootstrap files haftmann parents: 37118 diff changeset	1
19e8b730ddeb tuned bootstrap files haftmann parents: 37118 diff changeset	2	(* Classical Higher-order Logic -- batteries included *)
19e8b730ddeb tuned bootstrap files haftmann parents: 37118 diff changeset	3
44561 73f84bf0c6ac avoid loading List_Cset and Dlist_Cet at the same time haftmann parents: 44006 diff changeset	4	use_thys ["Library", "List_Cset", "List_Prefix", "List_lexord", "Sublist_Order",
44006 b9839fad3bb6 new theory HOL/Library/Product_Lattice.thy huffman parents: 42841 diff changeset	5	"Product_Lattice",
45483 34d07cf7d207 add Code_Real_Approx_By_Float hoelzl parents: 44561 diff changeset	6	"Code_Char_chr", "Code_Char_ord", "Code_Integer", "Efficient_Nat", "Executable_Set"(, "Code_Prolog"),
34d07cf7d207 add Code_Real_Approx_By_Float hoelzl parents: 44561 diff changeset	7	"Code_Real_Approx_By_Float" ];