isabelle: src/HOL/Library/ROOT.ML@73f84bf0c6ac (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",
42841 9079f49053e5 adding theory to force code generation of ordering on characters to built-in ordering of characters in target languages bulwahn parents: 38504 diff changeset	6	"Code_Char_chr", "Code_Char_ord", "Code_Integer", "Efficient_Nat", "Executable_Set"(, "Code_Prolog")];