src/sml/IsacKnowledge/Integrate.thy
changeset 2918 cac1f942e1a1
parent 2916 730089aebfcf
child 3747 2fae9b163442
     1.1 --- a/src/sml/IsacKnowledge/Integrate.thy	Sat Aug 20 19:10:30 2005 +0200
     1.2 +++ b/src/sml/IsacKnowledge/Integrate.thy	Sat Aug 20 21:20:16 2005 +0200
     1.3 @@ -27,7 +27,7 @@
     1.4  
     1.5    (*Script-names*)
     1.6    IntegrationScript      :: "[real,real,  real] => real"
     1.7 -                  ("((Script IntegrationScript (_ _=))// (_))" 9)
     1.8 +                  ("((Script IntegrationScript (_ _ =))// (_))" 9)
     1.9    NamedIntegrationScript :: "[real,real,real,  bool] => bool"
    1.10                    ("((Script NamedIntegrationScript (_ _ _=))// (_))" 9)
    1.11