equal
deleted
inserted
replaced
95 (*+*)val Rule_Set.Repeat {id = "prls_met_test_squ_sub", ...} = where_rls |
95 (*+*)val Rule_Set.Repeat {id = "prls_met_test_squ_sub", ...} = where_rls |
96 (*+*)val [(true, tTEST as Const ("Test.precond_rootmet", _) $ Free ("x", xxx))] = full_subst |
96 (*+*)val [(true, tTEST as Const ("Test.precond_rootmet", _) $ Free ("x", xxx))] = full_subst |
97 |
97 |
98 (*+*)val ctxt = Config.put rewrite_trace true ctxt; |
98 (*+*)val ctxt = Config.put rewrite_trace true ctxt; |
99 val evals = map ( |
99 val evals = map ( |
100 Pre_Conds.eval ctxt where_rls) pres'; |
100 Pre_Conds.eval ctxt where_rls) full_subst; |
101 (* (*declare [[rewrite_trace = true]]*) |
101 (* (*declare [[rewrite_trace = true]]*) |
102 @## rls: prls_met_test_squ_sub on: precond_rootmet x |
102 @## rls: prls_met_test_squ_sub on: precond_rootmet x |
103 @### try calc: "Test.precond_rootmet" |
103 @### try calc: "Test.precond_rootmet" |
104 @#### eval asms: "(precond_rootmet x) = True" |
104 @#### eval asms: "(precond_rootmet x) = True" |
105 @### calc. to: True |
105 @### calc. to: True |