equal
deleted
inserted
replaced
1082 |
1082 |
1083 |
1083 |
1084 |
1084 |
1085 (** outer syntax **) |
1085 (** outer syntax **) |
1086 |
1086 |
1087 val print_clasetP = |
1087 val _ = |
1088 OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner" |
1088 OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner" |
1089 OuterKeyword.diag |
1089 OuterKeyword.diag |
1090 (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep |
1090 (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o (Toplevel.keep |
1091 (Toplevel.node_case |
1091 (Toplevel.node_case |
1092 (Context.cases print_claset print_local_claset) |
1092 (Context.cases print_claset print_local_claset) |
1093 (print_local_claset o Proof.context_of))))); |
1093 (print_local_claset o Proof.context_of))))); |
1094 |
1094 |
1095 val _ = OuterSyntax.add_parsers [print_clasetP]; |
|
1096 |
|
1097 |
|
1098 end; |
1095 end; |