equal
deleted
inserted
replaced
4 |
4 |
5 12345678901234567890123456789012345678901234567890123456789012345678901234567890 |
5 12345678901234567890123456789012345678901234567890123456789012345678901234567890 |
6 10 20 30 40 50 60 70 80 |
6 10 20 30 40 50 60 70 80 |
7 *) |
7 *) |
8 |
8 |
9 theory Atools imports Descript Typefix (*...WOULD BE REQUIRED*) |
9 theory Atools imports Descript begin |
10 (*theory Atools imports Complex_Main*) |
|
11 (*theory Atools imports "../Knowledge/Descript" "../Knowledge/Typefix" begin*) |
|
12 uses ("../ProgLang/term.sml") |
|
13 begin |
|
14 use "../ProgLang/term.sml" |
|
15 |
10 |
16 consts |
11 consts |
17 |
12 |
18 Arbfix :: "real" |
13 Arbfix :: "real" |
19 Undef :: "real" |
14 Undef :: "real" |
540 Calc ("Atools.ident",eval_ident "#ident_"), |
535 Calc ("Atools.ident",eval_ident "#ident_"), |
541 Calc ("op =",eval_equal "#equal_"),(*atom <> atom -> False*) |
536 Calc ("op =",eval_equal "#equal_"),(*atom <> atom -> False*) |
542 |
537 |
543 Calc ("Tools.Vars",eval_var "#Vars_"), |
538 Calc ("Tools.Vars",eval_var "#Vars_"), |
544 |
539 |
545 Thm ("if_True",num_str if_True), |
540 Thm ("if_True",num_str @{thm HOL.if_True}), |
546 Thm ("if_False",num_str if_False) |
541 Thm ("if_False",num_str @{thm HOL.if_False}) |
547 ]; |
542 ]; |
548 |
543 |
549 ruleset' := overwritelthy thy (!ruleset', |
544 ruleset' := overwritelthy thy (!ruleset', |
550 [("list_rls",list_rls) |
545 [("list_rls",list_rls) |
551 ]); |
546 ]); |