1.1 --- a/test/Tools/isac/Knowledge/eqsystem-2.sml	Sun Oct 09 09:01:29 2022 +0200
     1.2 +++ b/test/Tools/isac/Knowledge/eqsystem-2.sml	Wed Oct 19 10:43:04 2022 +0200
     1.3 @@ -2,30 +2,27 @@
     1.4     author: Walther Neuper 050826,
     1.5     (c) due to copyright terms
     1.6  *)
     1.7 -
     1.8 -"-----------------------------------------------------------------";
     1.9 -"table of contents -----------------------------------------------";
    1.10 -"-----------------------------------------------------------------";
    1.11 -"----------- occur_exactly_in ------------------------------------";
    1.12 -"----------- problems --------------------------------------------";
    1.13 -"----------- rewrite-order ord_simplify_System -------------------";
    1.14 -"----------- rewrite in [EqSystem,normalise,2x2] -----------------";
    1.15 -"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ---";
    1.16 -"----------- rewrite in [EqSystem,top_down_substitution,2x2] -----";
    1.17 -"----------- rewrite in [EqSystem,normalise,4x4] -----------------";
    1.18 -"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 --";
    1.19 -"----------- refine [linear,system]-------------------------------";
    1.20 -"----------- refine [2x2,linear,system] search error--------------";
    1.21 -(*^^^--- eqsystem-1.sml  #####################################################################*)
    1.22 -"----------- me [EqSystem,normalise,2x2], refine Subproblem ------------------------------------";
    1.23 -(*^^^--- eqsystem-1a.sml #####################################################################
    1.24 -  vvv--- eqsystem-2.sml  #####################################################################*)
    1.25 -"----------- me [linear,system] ..normalise..top_down_sub..-------";
    1.26 -"----------- all systems from Biegelinie -------------------------";
    1.27 -"----------- 4x4 systems from Biegelinie -------------------------";
    1.28 -"-----------------------------------------------------------------";
    1.29 -"-----------------------------------------------------------------";
    1.30 -"-----------------------------------------------------------------";
    1.31 +"-----------------------------------------------------------------------------------------------";
    1.32 +"table of contents -----------------------------------------------------------------------------";
    1.33 +"-----------------------------------------------------------------------------------------------";
    1.34 +"----------- occur_exactly_in ---------------------------------------------------equsystem-1.sml";
    1.35 +"----------- problems -----------------------------------------------------------equsystem-1.sml";
    1.36 +"----------- rewrite-order ord_simplify_System ----------------------------------equsystem-1.sml";
    1.37 +"----------- rewrite in [EqSystem,normalise,2x2] --------------------------------equsystem-1.sml";
    1.38 +"----------- rewrite example from 2nd [EqSystem,normalise,2x2] ------------------equsystem-1.sml";
    1.39 +"----------- rewrite in [EqSystem,top_down_substitution,2x2] --------------------equsystem-1.sml";
    1.40 +"----------- rewrite in [EqSystem,normalise,4x4] --------------------------------equsystem-1.sml";
    1.41 +"----------- script [EqSystem,top_down_substitution,2x2] Vers.1 -----------------equsystem-1.sml";
    1.42 +"----------- refine [linear,system]----------------------------------------------equsystem-1.sml";
    1.43 +"----------- refine [2x2,linear,system] search error-----------------------------equsystem-1.sml";
    1.44 +"----------- me [EqSystem,normalise,2x2], refine Subproblem ---------------------equsystem-1.sml";
    1.45 +"----------- me [EqSystem,normalise,2x2], refine Subproblem, step into istate---equsystem-1a.sml";
    1.46 +"----------- me [linear,system] ..normalise..top_down_sub..----------------------equsystem-2.sml";
    1.47 +"----------- all systems from Biegelinie ----------------------------------------equsystem-2.sml";
    1.48 +"----------- 4x4 systems from Biegelinie ----------------------------------------equsystem-2.sml";
    1.49 +"-----------------------------------------------------------------------------------------------";
    1.50 +"-----------------------------------------------------------------------------------------------";
    1.51 +"-----------------------------------------------------------------------------------------------";
    1.52  
    1.53  val thy = @{theory "EqSystem"};
    1.54  val ctxt = Proof_Context.init_global thy;