equal
deleted
inserted
replaced
693 *} |
693 *} |
694 |
694 |
695 (* Optional methods *) |
695 (* Optional methods *) |
696 |
696 |
697 method_setup trancl = |
697 method_setup trancl = |
698 {* Method.no_args (Method.SIMPLE_METHOD' Trancl_Tac.trancl_tac) *} |
698 {* Method.no_args (SIMPLE_METHOD' Trancl_Tac.trancl_tac) *} |
699 {* simple transitivity reasoner *} |
699 {* simple transitivity reasoner *} |
700 method_setup rtrancl = |
700 method_setup rtrancl = |
701 {* Method.no_args (Method.SIMPLE_METHOD' Trancl_Tac.rtrancl_tac) *} |
701 {* Method.no_args (SIMPLE_METHOD' Trancl_Tac.rtrancl_tac) *} |
702 {* simple transitivity reasoner *} |
702 {* simple transitivity reasoner *} |
703 method_setup tranclp = |
703 method_setup tranclp = |
704 {* Method.no_args (Method.SIMPLE_METHOD' Tranclp_Tac.trancl_tac) *} |
704 {* Method.no_args (SIMPLE_METHOD' Tranclp_Tac.trancl_tac) *} |
705 {* simple transitivity reasoner (predicate version) *} |
705 {* simple transitivity reasoner (predicate version) *} |
706 method_setup rtranclp = |
706 method_setup rtranclp = |
707 {* Method.no_args (Method.SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac) *} |
707 {* Method.no_args (SIMPLE_METHOD' Tranclp_Tac.rtrancl_tac) *} |
708 {* simple transitivity reasoner (predicate version) *} |
708 {* simple transitivity reasoner (predicate version) *} |
709 |
709 |
710 end |
710 end |