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>