src/Tools/isac/Knowledge/EqSystem.thy
changeset 60763 2121f1a39a64
parent 60675 d841c720d288
child 60767 466f0a5bfb73
equal deleted inserted replaced
60762:f10bbfb2b3bb 60763:2121f1a39a64
    11   occur_exactly_in :: 
    11   occur_exactly_in :: 
    12    "[real list, real list, 'a] => bool" ("_ from _ occur'_exactly'_in _")
    12    "[real list, real list, 'a] => bool" ("_ from _ occur'_exactly'_in _")
    13 
    13 
    14   (*descriptions in the related problems*)
    14   (*descriptions in the related problems*)
    15   solveForVars       :: "real list => toreall"
    15   solveForVars       :: "real list => toreall"
    16   solution           :: "bool list => toreall"
    16 solution           :: "bool list => toreall" (*\<longrightarrow> Input_Descript.thy: known by fun is_NObrack_list*)
    17 
    17 
    18   (*the CAS-command, eg. "solveSystem [x+y=1,y=2] [x,y]"*)
    18   (*the CAS-command, eg. "solveSystem [x+y=1,y=2] [x,y]"*)
    19   solveSystem        :: "[bool list, real list] => bool list"
    19   solveSystem        :: "[bool list, real list] => bool list"
    20 
    20 
    21 lemma commute_0_equality : \<open>(0 = a) = (a = 0)\<close>
    21 lemma commute_0_equality : \<open>(0 = a) = (a = 0)\<close>