src/Tools/isac/Knowledge/Simplify.thy
changeset 59551 6ea6d9c377a0
parent 59545 4035ec339062
child 59592 99c8d2ff63eb
     1.1 --- a/src/Tools/isac/Knowledge/Simplify.thy	Sat Jun 22 13:15:52 2019 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/Simplify.thy	Sat Jun 22 14:34:06 2019 +0200
     1.3 @@ -20,10 +20,6 @@
     1.4    Simplify    :: "real => real"  (*"Simplify (1+2a+3+4a)*)
     1.5    Vereinfache :: "real => real"  (*"Vereinfache (1+2a+3+4a)*)
     1.6  
     1.7 -  (*Script-name*)
     1.8 -  SimplifyScript      :: "[real,  real] => real"
     1.9 -                  ("((Script SimplifyScript (_ =))// (_))" 9)
    1.10 -
    1.11  ML \<open>
    1.12  val thy = @{theory};
    1.13  \<close>