equal
deleted
inserted
replaced
5 |
5 |
6 "-----------------------------------------------------------------------------------------------"; |
6 "-----------------------------------------------------------------------------------------------"; |
7 "table of contents -----------------------------------------------------------------------------"; |
7 "table of contents -----------------------------------------------------------------------------"; |
8 "-----------------------------------------------------------------------------------------------"; |
8 "-----------------------------------------------------------------------------------------------"; |
9 "-----------------------------------------------------------------------------------------------"; |
9 "-----------------------------------------------------------------------------------------------"; |
10 "----------- fun result, fun creates_assms ---------------------------------------------------"; |
10 "----------- fun result, fun creates_assms -----------------------------------------------------"; |
|
11 "----------- fun subst_adapt_to_type -----------------------------------------------------------"; |
11 "-----------------------------------------------------------------------------------------------"; |
12 "-----------------------------------------------------------------------------------------------"; |
12 "-----------------------------------------------------------------------------------------------"; |
13 "-----------------------------------------------------------------------------------------------"; |
13 "-----------------------------------------------------------------------------------------------"; |
14 "-----------------------------------------------------------------------------------------------"; |
14 |
15 |
15 "----------- fun result, fun creates_assms ---------------------------------------------------"; |
16 "----------- fun result, fun creates_assms ---------------------------------------------------"; |
21 Rewrite': ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * ThmC.T * term * Calc.result -> Tactic.T; |
22 Rewrite': ThyC.id * Rewrite_Ord.id * Rule_Set.T * bool * ThmC.T * term * Calc.result -> Tactic.T; |
22 val tac = Rewrite' ("Diff", "dummy_ord", Rule_Set.empty, true, thm'', f, res) |
23 val tac = Rewrite' ("Diff", "dummy_ord", Rule_Set.empty, true, thm'', f, res) |
23 ; |
24 ; |
24 if (Tactic.result tac |> UnparseC.term) = "a / b" then () else error "creates_assms CHANGED"; |
25 if (Tactic.result tac |> UnparseC.term) = "a / b" then () else error "creates_assms CHANGED"; |
25 if (Tactic.creates_assms tac |> UnparseC.terms) = "[\"k \<noteq> 0\"]" then () else error "creates_assms CHANGED"; |
26 if (Tactic.creates_assms tac |> UnparseC.terms) = "[\"k \<noteq> 0\"]" then () else error "creates_assms CHANGED"; |
|
27 |
|
28 |
|
29 "----------- fun subst_adapt_to_type -----------------------------------------------------------"; |
|
30 "----------- fun subst_adapt_to_type -----------------------------------------------------------"; |
|
31 "----------- fun subst_adapt_to_type -----------------------------------------------------------"; |
|
32 val subs = ["(''bdv'', x)"]; |
|
33 |
|
34 val [((Free ("bdv", T1)), Free ("x", T2))] = subst_adapt_to_type ctxt subs; |
|
35 if T1 = HOLogic.realT andalso T2 = HOLogic.realT |
|
36 then () else error "subst_adapt_to_type CHANGED"; |
|
37 |