equal
deleted
inserted
replaced
522 *} |
522 *} |
523 |
523 |
524 ML %grayML{*fun foc_tac {prems, params, asms, concl, context, schematics} = |
524 ML %grayML{*fun foc_tac {prems, params, asms, concl, context, schematics} = |
525 let |
525 let |
526 fun assgn1 f1 f2 xs = |
526 fun assgn1 f1 f2 xs = |
527 Pretty.list "" "" (map (fn (x, y) => Pretty.enum ":=" "" "" [f1 x, f2 y]) xs) |
527 let |
|
528 val out = map (fn (x, y) => Pretty.enum ":=" "" "" [f1 x, f2 y]) xs |
|
529 in |
|
530 Pretty.list "" "" out |
|
531 end |
528 |
532 |
529 fun assgn2 f xs = assgn1 f f xs |
533 fun assgn2 f xs = assgn1 f f xs |
530 |
534 |
531 val pps = map (fn (s, pp) => Pretty.block [Pretty.str s, pp]) |
535 val pps = map (fn (s, pp) => Pretty.block [Pretty.str s, pp]) |
532 [("params: ", assgn1 Pretty.str (pretty_cterm context) params), |
536 [("params: ", assgn1 Pretty.str (pretty_cterm context) params), |
556 The tactic produces the following printout: |
560 The tactic produces the following printout: |
557 |
561 |
558 \begin{quote}\small |
562 \begin{quote}\small |
559 \begin{tabular}{ll} |
563 \begin{tabular}{ll} |
560 params: & @{text "x:= x"}, @{text "y:= y"}\\ |
564 params: & @{text "x:= x"}, @{text "y:= y"}\\ |
561 schematics: & @{text "?z:=z"}\\ |
|
562 assumptions: & @{term "A x y"}\\ |
565 assumptions: & @{term "A x y"}\\ |
563 conclusion: & @{term "B y x \<longrightarrow> C (z y) x"}\\ |
566 conclusion: & @{term "B y x \<longrightarrow> C (z y) x"}\\ |
564 premises: & @{term "A x y"} |
567 premises: & @{term "A x y"}\\ |
|
568 schematics: & @{text "?z:=z"} |
565 \end{tabular} |
569 \end{tabular} |
566 \end{quote} |
570 \end{quote} |
567 |
571 |
568 The @{text params} and @{text schematics} stand for list of pairs where the |
572 The @{text params} and @{text schematics} stand for list of pairs where the |
569 left-hand side of @{text ":="} is replaced by the right-hand side inside the |
573 left-hand side of @{text ":="} is replaced by the right-hand side inside the |
584 then the tactic prints out: |
588 then the tactic prints out: |
585 |
589 |
586 \begin{quote}\small |
590 \begin{quote}\small |
587 \begin{tabular}{ll} |
591 \begin{tabular}{ll} |
588 params: & @{text "x:= x"}, @{text "y:= y"}\\ |
592 params: & @{text "x:= x"}, @{text "y:= y"}\\ |
589 schematics: & @{text "?z:=z"}\\ |
|
590 assumptions: & @{term "A x y"}, @{term "B y x"}\\ |
593 assumptions: & @{term "A x y"}, @{term "B y x"}\\ |
591 conclusion: & @{term "C (z y) x"}\\ |
594 conclusion: & @{term "C (z y) x"}\\ |
592 premises: & @{term "A x y"}, @{term "B y x"} |
595 premises: & @{term "A x y"}, @{term "B y x"}\\ |
|
596 schematics: & @{text "?z:=z"} |
593 \end{tabular} |
597 \end{tabular} |
594 \end{quote} |
598 \end{quote} |
595 *} |
599 *} |
596 (*<*)oops(*>*) |
600 (*<*)oops(*>*) |
597 |
601 |