src/Pure/Isar/isar_syn.ML
changeset 13284 20c818c966e6
parent 13275 fdd23370b98f
child 13373 33b7736d8cc0
equal deleted inserted replaced
13283:1051aa66cbf3 13284:20c818c966e6
   581     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations));
   581     (Scan.succeed (Toplevel.no_timing o IsarCmd.print_antiquotations));
   582 
   582 
   583 val thms_containingP =
   583 val thms_containingP =
   584   OuterSyntax.improper_command "thms_containing"
   584   OuterSyntax.improper_command "thms_containing"
   585     "print facts containing certain constants or variables"
   585     "print facts containing certain constants or variables"
   586     K.diag (Scan.repeat P.term >> (Toplevel.no_timing oo IsarCmd.print_thms_containing));
   586     K.diag (Scan.option (P.$$$ "(" |-- P.!!! (P.nat --| P.$$$ ")")) --
       
   587       Scan.repeat P.term >> (Toplevel.no_timing oo IsarCmd.print_thms_containing));
   587 
   588 
   588 val thm_depsP =
   589 val thm_depsP =
   589   OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"
   590   OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"
   590     K.diag (P.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
   591     K.diag (P.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
   591 
   592