src/sml/IsacKnowledge/Integrate.thy
changeset 2918 cac1f942e1a1
parent 2916 730089aebfcf
child 3747 2fae9b163442
equal deleted inserted replaced
2917:2488337fd0dd 2918:cac1f942e1a1
    25   (*the CAS-command*)
    25   (*the CAS-command*)
    26   Integrate        :: "[real * real] => real"  (* "integrate (2*x^^^3, x)" *)
    26   Integrate        :: "[real * real] => real"  (* "integrate (2*x^^^3, x)" *)
    27 
    27 
    28   (*Script-names*)
    28   (*Script-names*)
    29   IntegrationScript      :: "[real,real,  real] => real"
    29   IntegrationScript      :: "[real,real,  real] => real"
    30                   ("((Script IntegrationScript (_ _=))// (_))" 9)
    30                   ("((Script IntegrationScript (_ _ =))// (_))" 9)
    31   NamedIntegrationScript :: "[real,real,real,  bool] => bool"
    31   NamedIntegrationScript :: "[real,real,real,  bool] => bool"
    32                   ("((Script NamedIntegrationScript (_ _ _=))// (_))" 9)
    32                   ("((Script NamedIntegrationScript (_ _ _=))// (_))" 9)
    33 
    33 
    34 rules 
    34 rules 
    35 (*stated as axioms, todo: prove as theorems
    35 (*stated as axioms, todo: prove as theorems