1 (* Title: Knowledge/eqsystem-2.sml |
1 (* Title: Knowledge/eqsystem-2.sml |
2 author: Walther Neuper 050826, |
2 author: Walther Neuper 050826, |
3 (c) due to copyright terms |
3 (c) due to copyright terms |
4 *) |
4 *) |
5 |
5 "-----------------------------------------------------------------------------------------------"; |
6 "-----------------------------------------------------------------"; |
6 "table of contents -----------------------------------------------------------------------------"; |
7 "table of contents -----------------------------------------------"; |
7 "-----------------------------------------------------------------------------------------------"; |
8 "-----------------------------------------------------------------"; |
8 "----------- occur_exactly_in ---------------------------------------------------equsystem-1.sml"; |
9 "----------- occur_exactly_in ------------------------------------"; |
9 "----------- problems -----------------------------------------------------------equsystem-1.sml"; |
10 "----------- problems --------------------------------------------"; |
10 "----------- rewrite-order ord_simplify_System ----------------------------------equsystem-1.sml"; |
11 "----------- rewrite-order ord_simplify_System -------------------"; |
11 "----------- rewrite in [EqSystem,normalise,2x2] --------------------------------equsystem-1.sml"; |
12 "----------- rewrite in [EqSystem,normalise,2x2] -----------------"; |
12 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ------------------equsystem-1.sml"; |
13 "----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---"; |
13 "----------- rewrite in [EqSystem,top_down_substitution,2x2] --------------------equsystem-1.sml"; |
14 "----------- rewrite in [EqSystem,top_down_substitution,2x2] -----"; |
14 "----------- rewrite in [EqSystem,normalise,4x4] --------------------------------equsystem-1.sml"; |
15 "----------- rewrite in [EqSystem,normalise,4x4] -----------------"; |
15 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 -----------------equsystem-1.sml"; |
16 "----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --"; |
16 "----------- refine [linear,system]----------------------------------------------equsystem-1.sml"; |
17 "----------- refine [linear,system]-------------------------------"; |
17 "----------- refine [2x2,linear,system] search error-----------------------------equsystem-1.sml"; |
18 "----------- refine [2x2,linear,system] search error--------------"; |
18 "----------- me [EqSystem,normalise,2x2], refine Subproblem ---------------------equsystem-1.sml"; |
19 (*^^^--- eqsystem-1.sml #####################################################################*) |
19 "----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml"; |
20 "----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------"; |
20 "----------- me [linear,system] ..normalise..top_down_sub..----------------------equsystem-2.sml"; |
21 (*^^^--- eqsystem-1a.sml ##################################################################### |
21 "----------- all systems from Biegelinie ----------------------------------------equsystem-2.sml"; |
22 vvv--- eqsystem-2.sml #####################################################################*) |
22 "----------- 4x4 systems from Biegelinie ----------------------------------------equsystem-2.sml"; |
23 "----------- me [linear,system] ..normalise..top_down_sub..-------"; |
23 "-----------------------------------------------------------------------------------------------"; |
24 "----------- all systems from Biegelinie -------------------------"; |
24 "-----------------------------------------------------------------------------------------------"; |
25 "----------- 4x4 systems from Biegelinie -------------------------"; |
25 "-----------------------------------------------------------------------------------------------"; |
26 "-----------------------------------------------------------------"; |
|
27 "-----------------------------------------------------------------"; |
|
28 "-----------------------------------------------------------------"; |
|
29 |
26 |
30 val thy = @{theory "EqSystem"}; |
27 val thy = @{theory "EqSystem"}; |
31 val ctxt = Proof_Context.init_global thy; |
28 val ctxt = Proof_Context.init_global thy; |
32 |
29 |
33 "----------- me [linear,system] ..normalise..top_down_sub..-------"; |
30 "----------- me [linear,system] ..normalise..top_down_sub..-------"; |