src/sml/IsacKnowledge/Simplify.thy
author wneuper
Thu, 17 Jan 2008 16:27:03 +0100
changeset 3881 72f0be16d83b
parent 3750 a7c05e185c94
permissions -rw-r--r--
start-work-070517 merged into HEAD
wneuper@3750
     1
(* simplification of terms
wneuper@3750
     2
   author: Walther Neuper 050912
wneuper@3750
     3
   (c) due to copyright terms
wneuper@3750
     4
wneuper@3750
     5
remove_thy"Simplify";
wneuper@3750
     6
use_thy"~/proto2/isac/src/sml/IsacKnowledge/Simplify";
wneuper@3750
     7
wneuper@3750
     8
use_thy_only"~/proto2/isac/src/sml/IsacKnowledge/Simplify";
wneuper@3750
     9
use_thy"~/proto2/isac/src/sml/IsacKnowledge/Isac";
wneuper@3750
    10
*)
wneuper@3750
    11
wneuper@3750
    12
Simplify = Atools +
wneuper@3750
    13
wneuper@3750
    14
consts
wneuper@3750
    15
wneuper@3750
    16
  (*descriptions in the related problem*)
wneuper@3881
    17
  term        :: real => una
wneuper@3881
    18
  normalform  :: real => una
wneuper@3750
    19
wneuper@3750
    20
  (*the CAS-command*)
wneuper@3881
    21
  Simplify    :: "real => real"  (*"Simplify (1+2a+3+4a)*)
wneuper@3881
    22
  Vereinfache :: "real => real"  (*"Vereinfache (1+2a+3+4a)*)
wneuper@3750
    23
wneuper@3750
    24
  (*Script-name*)
wneuper@3750
    25
  SimplifyScript      :: "[real,  real] => real"
wneuper@3750
    26
                  ("((Script SimplifyScript (_ =))// (_))" 9)
wneuper@3750
    27
wneuper@3750
    28
wneuper@3750
    29
end