61 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
61 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
62 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
62 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
63 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
63 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
64 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["EqSystem", "top_down_substitution", "2x2"] = nxt |
64 val (p,_,f,nxt,_,pt) = me nxt p c pt; val Specify_Method ["EqSystem", "top_down_substitution", "2x2"] = nxt |
65 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
65 val (p,_,f,nxt,_,pt) = me nxt p c pt; |
|
66 |
66 val PblObj {probl,...} = get_obj I pt [5]; |
67 val PblObj {probl,...} = get_obj I pt [5]; |
67 (writeln o (I_Model.to_string (Proof_Context.init_global @{theory Isac_Knowledge}))) probl; |
68 |
68 (*[ |
|
69 (1 ,[1] ,true ,#Given ,Cor equalities [c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2] ,(es_, [[c_2 = 0, L * c + c_2 = q_0 * L \<up> 2 / 2]])), |
|
70 (2 ,[1] ,true ,#Given ,Cor solveForVars [c, c_2] ,(v_s, [[c, c_2]])), |
|
71 (3 ,[1] ,true ,#Find ,Cor solution ss___ ,(ss___, [ss___]))] |
|
72 *) |
|
73 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
69 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
74 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
70 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
75 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
71 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
76 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
72 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
77 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |
73 val (p,_,f,nxt,_,pt) = me nxt p c pt;f2str f; |