BNF/Tools/bnf_def.ML:@{command_spec "print_bnfs"}
BNF/Tools/bnf_def.ML:@{command_spec "bnf_def"}
BNF/Tools/bnf_gfp.ML:@{command_spec "codata"}
BNF/Tools/bnf_lfp.ML:@{command_spec "data"}
BNF/Tools/bnf_wrap.ML:@{command_spec "wrap_data"}
Boogie/Tools/boogie_commands.ML:@{command_spec "boogie_open"}
Boogie/Tools/boogie_commands.ML:@{command_spec "boogie_vc"}
Boogie/Tools/boogie_commands.ML:@{command_spec "boogie_status"}
Boogie/Tools/boogie_commands.ML:@{command_spec "boogie_end"}
* HOLCF/Tools/Domain/domain.ML:@{command_spec "domain"}
HOLCF/Tools/Domain/domain_isomorphism.ML:@{command_spec "domain_isomorphism"}
* HOLCF/Tools/fixrec.ML:@{command_spec "fixrec"}
HOLCF/Tools/domaindef.ML:@{command_spec "domaindef"}
HOLCF/Tools/cpodef.ML:@{command_spec "pcpodef"}
HOLCF/Tools/cpodef.ML:@{command_spec "cpodef"}
Import/import_rule.ML:@{command_spec "import_file"}
Import/import_data.ML:@{command_spec "import_type_map"}
Import/import_data.ML:@{command_spec "import_const_map"}
Library/refute.ML:@{command_spec "refute"}
Library/refute.ML:@{command_spec "refute_params"}
Nominal/nominal_atoms.ML:@{command_spec "atom_decl"}
Nominal/nominal_inductive.ML:@{command_spec "nominal_inductive"}
Nominal/nominal_inductive.ML:@{command_spec "equivariance"}
Nominal/nominal_datatype.ML:@{command_spec "nominal_datatype"}
Nominal/nominal_inductive2.ML:@{command_spec "nominal_inductive2"}
Nominal/nominal_primrec.ML:@{command_spec "nominal_primrec"}
Orderings.thy:@{command_spec "print_orders"}
SPARK/Tools/spark_commands.ML:@{command_spec "spark_open"}
SPARK/Tools/spark_commands.ML:@{command_spec "spark_open_vcg"}
SPARK/Tools/spark_commands.ML:@{command_spec "spark_open_siv"}
SPARK/Tools/spark_commands.ML:@{command_spec "spark_proof_functions"}
SPARK/Tools/spark_commands.ML:@{command_spec "spark_types"}
SPARK/Tools/spark_commands.ML:@{command_spec "spark_vc"}
SPARK/Tools/spark_commands.ML:@{command_spec "spark_status"}
SPARK/Tools/spark_commands.ML:@{command_spec "spark_end"}
Statespace/state_space.ML:@{command_spec "statespace"}
Tools/choice_specification.ML:@{command_spec "specification"}
Tools/choice_specification.ML:@{command_spec "ax_specification"}
Tools/Predicate_Compile/code_prolog.ML:@{command_spec "values"}
Tools/Predicate_Compile/predicate_compile.ML:@{command_spec "code_pred"}
Tools/Predicate_Compile/predicate_compile.ML:@{command_spec "values"}
* Tools/Datatype/primrec.ML:@{command_spec "primrec"}
* Tools/Datatype/datatype.ML:@{command_spec "datatype"}
* Tools/Datatype/rep_datatype.ML:@{command_spec "rep_datatype"}
Tools/SMT/smt_config.ML:@{command_spec "smt_status"}
Tools/recdef.ML:@{command_spec "recdef"}
Tools/recdef.ML:@{command_spec "defer_recdef"}
Tools/recdef.ML:@{command_spec "recdef_tc"}
Tools/record.ML:@{command_spec "record"}
Tools/Lifting/lifting_info.ML:@{command_spec "print_quotmaps"}
Tools/Lifting/lifting_info.ML:@{command_spec "print_quotients"}
Tools/Lifting/lifting_def.ML:@{command_spec "lift_definition"}
Tools/Lifting/lifting_setup.ML:@{command_spec "setup_lifting"}
Tools/inductive.ML:@{command_spec "inductive"}
Tools/inductive.ML:@{command_spec "coinductive"}
Tools/inductive.ML:@{command_spec "inductive_cases"}
Tools/inductive.ML:@{command_spec "inductive_simps"}
Tools/inductive.ML:@{command_spec "print_inductives"}
Tools/Sledgehammer/sledgehammer_isar.ML:@{command_spec "sledgehammer"}
Tools/Sledgehammer/sledgehammer_isar.ML:@{command_spec "sledgehammer_params"}
Tools/inductive_set.ML:@{command_spec "inductive_set"}
Tools/inductive_set.ML:@{command_spec "coinductive_set"}
* Tools/typedef.ML:@{command_spec "typedef"}
* Tools/Function/fun.ML:@{command_spec "fun"}
* Tools/Function/partial_function.ML:@{command_spec "partial_function"}
* Tools/Function/function.ML:@{command_spec "function"}
* Tools/Function/function.ML:@{command_spec "termination"}
Tools/try0.ML:@{command_spec "try0"}
Tools/Quickcheck/find_unused_assms.ML:@{command_spec "find_unused_assms"}
Tools/Quickcheck/abstract_generators.ML:@{command_spec "quickcheck_generator"}
Tools/Nitpick/nitpick_isar.ML:@{command_spec "nitpick"}
Tools/Nitpick/nitpick_isar.ML:@{command_spec "nitpick_params"}
Tools/enriched_type.ML:@{command_spec "enriched_type"}
Tools/Quotient/quotient_type.ML:@{command_spec "quotient_type"}
Tools/Quotient/quotient_info.ML:@{command_spec "print_quotmapsQ3"}
Tools/Quotient/quotient_info.ML:@{command_spec "print_quotientsQ3"}
Tools/Quotient/quotient_info.ML:@{command_spec "print_quotconsts"}
Tools/Quotient/quotient_def.ML:@{command_spec "quotient_definition"}
TPTP/TPTP_Parser/tptp_interpret.ML:@{command_spec "import_tptp"}