src/Tools/isac/Build_Isac.thy
branchisac-update-Isa09-2
changeset 37988 03e6d5db883e
parent 37985 0be0c4e7ab9e
child 37989 468809a52c9f
equal deleted inserted replaced
37987:bf83d30839c7 37988:03e6d5db883e
    67 use_thy "Knowledge/Rational"
    67 use_thy "Knowledge/Rational"
    68 use_thy "Knowledge/PolyMinus"
    68 use_thy "Knowledge/PolyMinus"
    69 use_thy "Knowledge/Equation"
    69 use_thy "Knowledge/Equation"
    70 use_thy "Knowledge/LinEq"
    70 use_thy "Knowledge/LinEq"
    71 use_thy "Knowledge/Root"
    71 use_thy "Knowledge/Root"
       
    72 use_thy "Knowledge/RootEq"
    72 
    73 
    73 
    74 
    74 ML {* 
    75 use_thy "Knowledge/RatEq"
    75 incr_boundvars;
       
    76 *}
       
    77 
       
    78 use_thy "Knowledge/RootEq"
       
    79 
    76 
    80 
    77 
    81 ML {* 
    78 ML {* 
    82 *}
    79 *}
    83 
    80 
    84 
    81 
    85 text {*------------------------------------------*}
    82 text {*------------------------------------------*}
    86 (*
    83 (*
    87 use_thy "Knowledge/RatEq"
       
    88 use_thy "Knowledge/RootRat"
    84 use_thy "Knowledge/RootRat"
    89 use_thy "Knowledge/RootRatEq"
    85 use_thy "Knowledge/RootRatEq"
    90 use_thy "Knowledge/PolyEq"
    86 use_thy "Knowledge/PolyEq"
    91 use_thy "Knowledge/Vect"
    87 use_thy "Knowledge/Vect"
    92 use_thy "Knowledge/Calculus"
    88 use_thy "Knowledge/Calculus"