Merge branch 'feature/wp/induction-tactic' into 'master'
[wp] induction tactic See merge request frama-c/frama-c!2933
Showing
- headers/header_spec.txt 2 additions, 0 deletionsheaders/header_spec.txt
- src/plugins/wp/Conditions.mli 1 addition, 1 deletionsrc/plugins/wp/Conditions.mli
- src/plugins/wp/GuiTactic.ml 1 addition, 0 deletionssrc/plugins/wp/GuiTactic.ml
- src/plugins/wp/Makefile.in 1 addition, 1 deletionsrc/plugins/wp/Makefile.in
- src/plugins/wp/TacInduction.ml 119 additions, 0 deletionssrc/plugins/wp/TacInduction.ml
- src/plugins/wp/TacInduction.mli 29 additions, 0 deletionssrc/plugins/wp/TacInduction.mli
- src/plugins/wp/doc/manual/wp_plugin.tex 117 additions, 98 deletionssrc/plugins/wp/doc/manual/wp_plugin.tex
- src/plugins/wp/tests/wp_tip/induction.i 28 additions, 0 deletionssrc/plugins/wp/tests/wp_tip/induction.i
- src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.res.oracle 12 additions, 0 deletions...gins/wp/tests/wp_tip/oracle_qualif/induction.0.res.oracle
- src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.session/script/lemma_ByInd.json 12 additions, 0 deletions...oracle_qualif/induction.0.session/script/lemma_ByInd.json
- src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.res.oracle 10 additions, 0 deletions...gins/wp/tests/wp_tip/oracle_qualif/induction.1.res.oracle
- src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.session/script/lemma_ByInd.json 12 additions, 0 deletions...oracle_qualif/induction.1.session/script/lemma_ByInd.json
- src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.res.oracle 10 additions, 0 deletions...gins/wp/tests/wp_tip/oracle_qualif/induction.2.res.oracle
- src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.session/script/lemma_ByInd.json 12 additions, 0 deletions...oracle_qualif/induction.2.session/script/lemma_ByInd.json
- src/plugins/wp/tests/wp_tip/oracle_qualif/induction.res.oracle 10 additions, 0 deletions...lugins/wp/tests/wp_tip/oracle_qualif/induction.res.oracle
- src/plugins/wp/tests/wp_tip/oracle_qualif/induction_prove.0.session/script/lemma_ByInd.json 13 additions, 0 deletions..._qualif/induction_prove.0.session/script/lemma_ByInd.json
Loading
Please register or sign in to comment