equal
deleted
inserted
replaced
219 "schematic_lemma" |
219 "schematic_lemma" |
220 "schematic_theorem" |
220 "schematic_theorem" |
221 "sect" |
221 "sect" |
222 "section" |
222 "section" |
223 "setup" |
223 "setup" |
|
224 "setup_lifting" |
224 "show" |
225 "show" |
225 "simproc_setup" |
226 "simproc_setup" |
226 "sledgehammer" |
227 "sledgehammer" |
227 "sledgehammer_params" |
228 "sledgehammer_params" |
228 "smt_status" |
229 "smt_status" |
516 "primrec" |
517 "primrec" |
517 "print_ast_translation" |
518 "print_ast_translation" |
518 "print_translation" |
519 "print_translation" |
519 "quickcheck_generator" |
520 "quickcheck_generator" |
520 "quickcheck_params" |
521 "quickcheck_params" |
521 "quotient_definition" |
|
522 "realizability" |
522 "realizability" |
523 "realizers" |
523 "realizers" |
524 "recdef" |
524 "recdef" |
525 "record" |
525 "record" |
526 "refute_params" |
526 "refute_params" |
527 "setup" |
527 "setup" |
|
528 "setup_lifting" |
528 "simproc_setup" |
529 "simproc_setup" |
529 "sledgehammer_params" |
530 "sledgehammer_params" |
530 "spark_end" |
531 "spark_end" |
531 "spark_open" |
532 "spark_open" |
532 "spark_proof_functions" |
533 "spark_proof_functions" |
561 "lemma" |
562 "lemma" |
562 "nominal_inductive" |
563 "nominal_inductive" |
563 "nominal_inductive2" |
564 "nominal_inductive2" |
564 "nominal_primrec" |
565 "nominal_primrec" |
565 "pcpodef" |
566 "pcpodef" |
|
567 "quotient_definition" |
566 "quotient_type" |
568 "quotient_type" |
567 "recdef_tc" |
569 "recdef_tc" |
568 "rep_datatype" |
570 "rep_datatype" |
569 "schematic_corollary" |
571 "schematic_corollary" |
570 "schematic_lemma" |
572 "schematic_lemma" |