src/Provers/classical.ML
changeset 8667 4230d17073ea
parent 8519 981f52707e5d
child 8671 6ce91a80f616
     1.1 --- a/src/Provers/classical.ML	Tue Apr 04 18:08:08 2000 +0200
     1.2 +++ b/src/Provers/classical.ML	Tue Apr 04 22:16:11 2000 +0200
     1.3 @@ -1181,4 +1181,16 @@
     1.4  val setup = [GlobalClaset.init, LocalClaset.init, setup_attrs, setup_methods];
     1.5  
     1.6  
     1.7 +
     1.8 +(** outer syntax **)
     1.9 +
    1.10 +val print_clasetP =
    1.11 +  OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner"
    1.12 +    OuterSyntax.Keyword.diag
    1.13 +    (Scan.succeed (Toplevel.keep
    1.14 +      (Toplevel.node_case print_claset (print_local_claset o Proof.context_of))));
    1.15 +
    1.16 +val _ = OuterSyntax.add_parsers [print_clasetP];
    1.17 +
    1.18 +
    1.19  end;