src/HOL/ROOT
changeset 48721 866f6d5baf4c
parent 48690 c1499b14b48c
child 48738 f8c1a5b9488f
equal deleted inserted replaced
48720:95669b431edd 48721:866f6d5baf4c
    34     Product_Lattice
    34     Product_Lattice
    35     Code_Char_chr
    35     Code_Char_chr
    36     Code_Char_ord
    36     Code_Char_ord
    37     Code_Integer
    37     Code_Integer
    38     Efficient_Nat
    38     Efficient_Nat
    39     (*"Code_Prolog" FIXME cf. 76965c356d2a *)
    39     (* Code_Prolog  FIXME cf. 76965c356d2a *)
    40     Code_Real_Approx_By_Float
    40     Code_Real_Approx_By_Float
    41     Target_Numeral
    41     Target_Numeral
    42   files "document/root.bib" "document/root.tex"
    42   files "document/root.bib" "document/root.tex"
    43 
    43 
    44 session Hahn_Banach = HOL +
    44 session Hahn_Banach = HOL +