isahipster: Commit: 6b80048a589cb841f04e8a826f4cf609dde81643

Branch: master

Author: Irene Lobo Valbuena <airinilv@gmail.com>
Date: Thu Mar 10 02:40:02 PM UTC 2016
Commit: 6b80048a589cb841f04e8a826f4cf609dde81643
Parent: ffe48f647ed5686e8843056bb874f81af574fe92 (diff to parent)
Log message:

    Isa 16 update

README.md (old)                                                   (diff) | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

Files:

• .gitignore (raw)
• HipsterExplore.ML (raw)
• HipsterIsar.ML (raw)
• HipsterTacs.ML (raw)
• HipsterUtils.ML (raw)
• HipTacOps.ML (raw)
• IndTacs.ML (raw)
• IsaHipster.thy (raw)
• README.md (raw)
• SchemeInstances.ML (raw)
• SledgehammerTacs.ML (raw)
• TacticData.ML (raw)
• ThyExplData.ML (raw)
• AVoCS2015
  • background.tex (raw)
  • bibfile.bib (raw)
  • conclusion.tex (raw)
  • conditionals.tex (raw)
  • easst.eps (raw)
  • easst.pdf (raw)
  • eceasst.bst (raw)
  • eceasst.cls (raw)
  • eval.tex (raw)
  • frontmatter.tex (raw)
  • hipsterAVoCS15.tex (raw)
  • hipster.pdf (raw)
  • introduction.tex (raw)
  • mathpartir.sty (raw)
  • preface.tex (raw)
  • rec-ind.tex (raw)
  • related.tex (raw)
• benchmark
  • Master.thy (raw)
  • temp.thy (raw)
  • airini
    • prop_01.thy (raw)
    • prop_02.thy (raw)
    • prop_03.thy (raw)
    • prop_04.thy (raw)
    • prop_05.thy (raw)
    • prop_07.thy (raw)
    • prop_08.thy (raw)
    • prop_09.thy (raw)
    • prop_10.thy (raw)
    • prop_11.thy (raw)
    • prop_12.thy (raw)
    • prop_13.thy (raw)
    • prop_14.thy (raw)
    • prop_15.thy (raw)
    • prop_16.thy (raw)
    • prop_17.thy (raw)
    • prop_18.thy (raw)
    • prop_19.thy (raw)
    • prop_20.thy (raw)
    • prop_21.thy (raw)
    • prop_22.thy (raw)
    • prop_23.thy (raw)
    • prop_24.thy (raw)
    • prop_25.thy (raw)
    • prop_26.thy (raw)
    • prop_27.thy (raw)
    • prop_28.thy (raw)
    • prop_29.thy (raw)
  • data
    • Heap.thy (raw)
    • list.thy (raw)
    • Natu.thy (raw)
    • Pair2.thy (raw)
    • Tree.thy (raw)
  • funcs
    • append.thy (raw)
    • butlastConcat.thy (raw)
    • butlast.thy (raw)
    • count.thy (raw)
    • delete.thy (raw)
    • double.thy (raw)
    • drop.thy (raw)
    • dropWhile.thy (raw)
    • elem.thy (raw)
    • eqN.thy (raw)
    • equal.thy (raw)
    • even.thy (raw)
    • exp.thy (raw)
    • fac.thy (raw)
    • filter.thy (raw)
    • half.thy (raw)
    • height.thy (raw)
    • ins1.thy (raw)
    • insert2.thy (raw)
    • insort.thy (raw)
    • ins.thy (raw)
    • intersect.thy (raw)
    • lastOfTwo.thy (raw)
    • last.thy (raw)
    • len.thy (raw)
    • le.thy (raw)
    • lt.thy (raw)
    • map.thy (raw)
    • max.thy (raw)
    • min.thy (raw)
    • minus.thy (raw)
    • mirror.thy (raw)
    • mult2.thy (raw)
    • mult.thy (raw)
    • null.thy (raw)
    • nunion.thy (raw)
    • one.thy (raw)
    • plus.thy (raw)
    • qexp.thy (raw)
    • qfac.thy (raw)
    • qrevflat.thy (raw)
    • qrev.thy (raw)
    • revflat.thy (raw)
    • rev.thy (raw)
    • rotate.thy (raw)
    • sorted.thy (raw)
    • sort.thy (raw)
    • subset.thy (raw)
    • take.thy (raw)
    • takeWhile.thy (raw)
    • unequal.thy (raw)
    • union.thy (raw)
    • zipConcat.thy (raw)
    • zip.thy (raw)
  • grammars
    • packrat_unambigPackrat.thy (raw)
    • simp_expr_unambig1.thy (raw)
    • simp_expr_unambig2.thy (raw)
    • simp_expr_unambig3.thy (raw)
    • simp_expr_unambig4.thy (raw)
    • simp_expr_unambig5.thy (raw)
  • isaplanner
    • benchList.thy (raw)
    • benchNat.thy (raw)
    • benchTree.thy (raw)
    • exploreBench.thy (raw)
    • isaplannerBench.thy (raw)
    • prop_01.thy (raw)
    • prop_02.thy (raw)
    • prop_03.thy (raw)
    • prop_04.thy (raw)
    • prop_05.thy (raw)
    • prop_06.thy (raw)
    • prop_07.thy (raw)
    • prop_08.thy (raw)
    • prop_09.thy (raw)
    • prop_10.thy (raw)
    • prop_11.thy (raw)
    • prop_12.thy (raw)
    • prop_13.thy (raw)
    • prop_14.thy (raw)
    • prop_15.thy (raw)
    • prop_16.thy (raw)
    • prop_17.thy (raw)
    • prop_18.thy (raw)
    • prop_19.thy (raw)
    • prop_20.thy (raw)
    • prop_21.thy (raw)
    • prop_22.thy (raw)
    • prop_23.thy (raw)
    • prop_24.thy (raw)
    • prop_25.thy (raw)
    • prop_26.thy (raw)
    • prop_27.thy (raw)
    • prop_28.thy (raw)
    • prop_29.thy (raw)
    • prop_30.thy (raw)
    • prop_31.thy (raw)
    • prop_32.thy (raw)
    • prop_33.thy (raw)
    • prop_34.thy (raw)
    • prop_35.thy (raw)
    • prop_36.thy (raw)
    • prop_37.thy (raw)
    • prop_38.thy (raw)
    • prop_39.thy (raw)
    • prop_40.thy (raw)
    • prop_41.thy (raw)
    • prop_42.thy (raw)
    • prop_43.thy (raw)
    • prop_44.thy (raw)
    • prop_45.thy (raw)
    • prop_46.thy (raw)
    • prop_47.thy (raw)
    • prop_48.thy (raw)
    • prop_49.thy (raw)
    • prop_50.thy (raw)
    • prop_51.thy (raw)
    • prop_52.thy (raw)
    • prop_53.thy (raw)
    • prop_54.thy (raw)
    • prop_55.thy (raw)
    • prop_56.thy (raw)
    • prop_57.thy (raw)
    • prop_58.thy (raw)
    • prop_59.thy (raw)
    • prop_60.thy (raw)
    • prop_61.thy (raw)
    • prop_62.thy (raw)
    • prop_63.thy (raw)
    • prop_64.thy (raw)
    • prop_65.thy (raw)
    • prop_66.thy (raw)
    • prop_67.thy (raw)
    • prop_68.thy (raw)
    • prop_69.thy (raw)
    • prop_70.thy (raw)
    • prop_71.thy (raw)
    • prop_72.thy (raw)
    • prop_73.thy (raw)
    • prop_74.thy (raw)
    • prop_75.thy (raw)
    • prop_76.thy (raw)
    • prop_77.thy (raw)
    • prop_78.thy (raw)
    • prop_79.thy (raw)
    • prop_80.thy (raw)
    • prop_81.thy (raw)
    • prop_82.thy (raw)
    • prop_83.thy (raw)
    • prop_84.thy (raw)
    • prop_85b.thy (raw)
    • prop_85.thy (raw)
    • prop_86.thy (raw)
    • testind.thy (raw)
    • Explored
      • count.thy (raw)
      • drop.thy (raw)
      • equal2.thy (raw)
      • equal.thy (raw)
      • max.thy (raw)
      • min.thy (raw)
      • minus.thy (raw)
      • plusminus.thy (raw)
      • plus.thy (raw)
      • take.thy (raw)
  • koen
    • list_append_inj_1.thy (raw)
    • list_append_inj_2.thy (raw)
    • list_Interleave.thy (raw)
    • list_PairEvens.thy (raw)
    • list_PairOdds.thy (raw)
    • list_PairUnpair.thy (raw)
    • list_SelectPermutations2.thy (raw)
    • list_SelectPermutations.thy (raw)
    • list_Select.thy (raw)
    • mccarthy91_M1.thy (raw)
    • mccarthy91_M2.thy (raw)
    • propositional_AndCommutative.thy (raw)
    • propositional_AndIdempotent.thy (raw)
    • propositional_AndImplication.thy (raw)
    • propositional_Okay.thy (raw)
    • propositional_Sound.thy (raw)
    • sort_BSortIsSort.thy (raw)
    • sort_BSortPermutes'.thy (raw)
    • sort_BSortPermutes.thy (raw)
    • sort_BSortSorts.thy (raw)
    • sort_BubSortIsSort.thy (raw)
    • sort_BubSortPermutes'.thy (raw)
    • sort_BubSortPermutes.thy (raw)
    • sort_BubSortSorts.thy (raw)
    • sort_HSortIsSort.thy (raw)
    • sort_HSortPermutes'.thy (raw)
    • sort_HSortPermutes.thy (raw)
    • sort_HSortSorts.thy (raw)
    • sort_ISortPermutes'.thy (raw)
    • sort_ISortPermutes.thy (raw)
    • sort_ISortSorts.thy (raw)
    • sort_MSortBU2IsSort.thy (raw)
    • sort_MSortBU2Permutes'.thy (raw)
    • sort_MSortBU2Permutes.thy (raw)
    • sort_MSortBU2Sorts.thy (raw)
    • sort_MSortBUIsSort.thy (raw)
    • sort_MSortBUPermutes'.thy (raw)
    • sort_MSortBUPermutes.thy (raw)
    • sort_MSortBUSorts.thy (raw)
    • sort_MSortTDIsSort.thy (raw)
    • sort_MSortTDPermutes'.thy (raw)
    • sort_MSortTDPermutes.thy (raw)
    • sort_MSortTDSorts.thy (raw)
    • sort_NMSortTDIsSort.thy (raw)
    • sort_NMSortTDPermutes'.thy (raw)
    • sort_NMSortTDPermutes.thy (raw)
    • sort_NMSortTDSorts.thy (raw)
    • sort_NStoogeSort2IsSort.thy (raw)
    • sort_NStoogeSort2Permutes'.thy (raw)
    • sort_NStoogeSort2Permutes.thy (raw)
    • sort_NStoogeSort2Sorts.thy (raw)
    • sort_NStoogeSortIsSort.thy (raw)
    • sort_NStoogeSortPermutes'.thy (raw)
    • sort_NStoogeSortPermutes.thy (raw)
    • sort_NStoogeSortSorts.thy (raw)
    • sort_QSortIsSort.thy (raw)
    • sort_QSortPermutes'.thy (raw)
    • sort_QSortPermutes.thy (raw)
    • sort_QSortSorts.thy (raw)
    • sort_SSortIsSort.thy (raw)
    • sort_SSortPermutes'.thy (raw)
    • sort_SSortPermutes.thy (raw)
    • sort_SSortSorts.thy (raw)
    • sort_StoogeSort2IsSort.thy (raw)
    • sort_StoogeSort2Permutes'.thy (raw)
    • sort_StoogeSort2Permutes.thy (raw)
    • sort_StoogeSort2Sorts.thy (raw)
    • sort_StoogeSortIsSort.thy (raw)
    • sort_StoogeSortPermutes'.thy (raw)
    • sort_StoogeSortPermutes.thy (raw)
    • sort_StoogeSortSorts.thy (raw)
    • sort_TSortIsSort.thy (raw)
    • sort_TSortPermutes'.thy (raw)
    • sort_TSortPermutes.thy (raw)
    • sort_TSortSorts.thy (raw)
    • subst_SubstFreeNo.thy (raw)
    • subst_SubstFreeYes.thy (raw)
    • tree_Flatten1List.thy (raw)
    • tree_Flatten1.thy (raw)
    • tree_Flatten2.thy (raw)
    • tree_Flatten3.thy (raw)
    • tree_SwapAB.thy (raw)
  • prod
    • prop_01.thy (raw)
    • prop_02.thy (raw)
    • prop_03.thy (raw)
    • prop_04.thy (raw)
    • prop_05.thy (raw)
    • prop_06.thy (raw)
    • prop_07.thy (raw)
    • prop_08.thy (raw)
    • prop_09.thy (raw)
    • prop_10.thy (raw)
    • prop_11.thy (raw)
    • prop_12.thy (raw)
    • prop_13.thy (raw)
    • prop_14.thy (raw)
    • prop_15.thy (raw)
    • prop_16.thy (raw)
    • prop_17.thy (raw)
    • prop_18.thy (raw)
    • prop_19.thy (raw)
    • prop_20.thy (raw)
    • prop_21.thy (raw)
    • prop_22.thy (raw)
    • prop_23.thy (raw)
    • prop_24.thy (raw)
    • prop_25.thy (raw)
    • prop_26.thy (raw)
    • prop_27.thy (raw)
    • prop_28.thy (raw)
    • prop_29.thy (raw)
    • prop_30.thy (raw)
    • prop_31.thy (raw)
    • prop_32.thy (raw)
    • prop_33.thy (raw)
    • prop_34.thy (raw)
    • prop_35.thy (raw)
    • prop_36.thy (raw)
    • prop_37.thy (raw)
    • prop_38.thy (raw)
    • prop_39.thy (raw)
    • prop_40.thy (raw)
    • prop_41.thy (raw)
    • prop_42.thy (raw)
    • prop_43.thy (raw)
    • prop_44.thy (raw)
    • prop_45.thy (raw)
    • prop_46.thy (raw)
    • prop_47.thy (raw)
    • prop_48.thy (raw)
    • prop_49.thy (raw)
    • prop_50.thy (raw)
  • scripts
    • all-isap.sh (raw)
    • hip-home.sh (raw)
  • tip2015
    • bin_distrib.thy (raw)
    • bin_plus_assoc.thy (raw)
    • bin_plus_comm.thy (raw)
    • bin_plus.thy (raw)
    • bin_s.thy (raw)
    • bin_times_assoc.thy (raw)
    • bin_times_comm.thy (raw)
    • bin_times.thy (raw)
    • escape_Injective.thy (raw)
    • escape_NoSpecial.thy (raw)
    • fermat_last.thy (raw)
    • heap_deleteMinimum.thy (raw)
    • heap_insert.thy (raw)
    • heap_merge.thy (raw)
    • heap_minimum.thy (raw)
    • heap_SortPermutes'.thy (raw)
    • heap_SortPermutes.thy (raw)
    • heap_SortSorts.thy (raw)
    • int_add_assoc.thy (raw)
    • int_add_comm.thy (raw)
    • int_add_ident_left.thy (raw)
    • int_add_ident_right.thy (raw)
    • int_add_inv_left.thy (raw)
    • int_add_inv_right.thy (raw)
    • int_left_distrib.thy (raw)
    • int_mul_assoc.thy (raw)
    • int_mul_comm.thy (raw)
    • int_mul_ident_left.thy (raw)
    • int_mul_ident_right.thy (raw)
    • int_right_distrib.thy (raw)
    • list_assoc.thy (raw)
    • list_concat_fmap_bind.thy (raw)
    • list_return_1.thy (raw)
    • list_return_2.thy (raw)
    • list_weird_concat_fmap_bind.thy (raw)
    • list_weird_is_normal.thy (raw)
    • nat_acc_alt_mul_assoc.thy (raw)
    • nat_acc_alt_mul_comm.thy (raw)
    • nat_acc_alt_mul_same.thy (raw)
    • nat_acc_plus_assoc.thy (raw)
    • nat_acc_plus_comm.thy (raw)
    • nat_acc_plus_same.thy (raw)
    • nat_alt_mul_assoc.thy (raw)
    • nat_alt_mul_comm.thy (raw)
    • nat_alt_mul_same.thy (raw)
    • nat_pow_le_factorial.thy (raw)
    • nat_pow_one.thy (raw)
    • nat_pow_pow.thy (raw)
    • nat_pow_times.thy (raw)
    • nicomachus_theorem.thy (raw)
    • regexp_Deeps.thy (raw)
    • regexp_PlusAssociative.thy (raw)
    • regexp_PlusCommutative.thy (raw)
    • regexp_PlusIdempotent.thy (raw)
    • regexp_RecAtom.thy (raw)
    • regexp_RecEps.thy (raw)
    • regexp_RecNil.thy (raw)
    • regexp_RecPlus.thy (raw)
    • regexp_RecSeq.thy (raw)
    • regexp_RecStar.thy (raw)
    • regexp_SeqAssociative.thy (raw)
    • regexp_SeqDistrPlus.thy (raw)
    • regexp_Star.thy (raw)
    • relaxedprefix_correct.thy (raw)
    • relaxedprefix_is_prefix_1.thy (raw)
    • relaxedprefix_is_prefix_2.thy (raw)
    • relaxedprefix_is_prefix_3.thy (raw)
    • relaxedprefix_is_prefix_4.thy (raw)
    • rotate_mod.thy (raw)
    • rotate_self.thy (raw)
    • rotate_snoc_self.thy (raw)
    • rotate_snoc.thy (raw)
    • rotate_structural_mod.thy (raw)
    • tree_sort_AddDifferent.thy (raw)
    • tree_sort_AddSame.thy (raw)
    • tree_sort_SortPermutes'.thy (raw)
    • tree_sort_SortPermutes.thy (raw)
    • tree_sort_SortSorts.thy (raw)
    • weird_nat_add3acc_assoc1.thy (raw)
    • weird_nat_add3acc_assoc2.thy (raw)
    • weird_nat_add3acc_assoc3.thy (raw)
    • weird_nat_add3acc_comm12.thy (raw)
    • weird_nat_add3acc_comm13.thy (raw)
    • weird_nat_add3acc_comm23.thy (raw)
    • weird_nat_add3acc_rot.thy (raw)
    • weird_nat_add3acc_rrot.thy (raw)
    • weird_nat_add3_assoc1.thy (raw)
    • weird_nat_add3_assoc2.thy (raw)
    • weird_nat_add3_assoc3.thy (raw)
    • weird_nat_add3_comm12.thy (raw)
    • weird_nat_add3_comm13.thy (raw)
    • weird_nat_add3_comm23.thy (raw)
    • weird_nat_add3_rot.thy (raw)
    • weird_nat_add3_rrot.thy (raw)
    • weird_nat_add3_same.thy (raw)
    • weird_nat_mul2_assoc.thy (raw)
    • weird_nat_mul2_comm.thy (raw)
    • weird_nat_mul3acc_assoc1.thy (raw)
    • weird_nat_mul3acc_assoc2.thy (raw)
    • weird_nat_mul3acc_assoc3.thy (raw)
    • weird_nat_mul3acc_comm12.thy (raw)
    • weird_nat_mul3acc_comm13.thy (raw)
    • weird_nat_mul3acc_comm23.thy (raw)
    • weird_nat_mul3acc_rot.thy (raw)
    • weird_nat_mul3acc_rrot.thy (raw)
    • weird_nat_mul3_assoc1.thy (raw)
    • weird_nat_mul3_assoc2.thy (raw)
    • weird_nat_mul3_assoc3.thy (raw)
    • weird_nat_mul3_comm12.thy (raw)
    • weird_nat_mul3_comm13.thy (raw)
    • weird_nat_mul3_comm23.thy (raw)
    • weird_nat_mul3_rot.thy (raw)
    • weird_nat_mul3_rrot.thy (raw)
    • weird_nat_mul3_same.thy (raw)
    • weird_nat_op_assoc2.thy (raw)
    • weird_nat_op_assoc.thy (raw)
    • weird_nat_op_comm_comm.thy (raw)
• CICM-paper
  • Background.tex (raw)
  • bibfile.bib (raw)
  • cicm-paper.tex (raw)
  • Conclusion.tex (raw)
  • hipster.odg (raw)
  • hipster.pdf (raw)
  • Hipster.tex (raw)
  • Introduction.tex (raw)
  • llncs.cls (raw)
  • llncsdoc.sty (raw)
  • PartialFunctions.tex (raw)
  • RelatedWork.tex (raw)
• Examples
  • BExp.thy (raw)
  • Cake.thy (raw)
  • Dev.thy (raw)
  • Exp.thy (raw)
  • ListDemo.thy (raw)
  • NatsBug.thy (raw)
  • SimpleCake.thy (raw)
  • SmallListDemo.thy (raw)
  • Sorted.thy (raw)
  • TreeDemo.thy (raw)
  • TreeSimp.thy (raw)
  • Tree.thy (raw)
  • 201509
    • dropTake.thy (raw)
    • prop_11.thy (raw)
    • Sorted.thy (raw)
  • proving
    • mirror (mirror x) == x
      • 0__0.mlw (raw)
      • 0__1.mlw (raw)
      • __0.mlw (raw)
• GenCode
  • .gitignore (raw)
  • .keepme (raw)
• hipspecifyer
  • hipspecifyer.cabal (raw)
  • HipSpecifyer.hs (raw)
  • LICENSE (raw)
  • HipSpecifyer
    • Prelude.hs (raw)
• LoboValbuena_slides
  • issues.md (raw)
  • Snips.hs (raw)
  • TermInducts.ML (raw)
  • demo
    • dropTake (raw)
    • dropTake.thy (raw)
    • prop_11.thy (raw)
    • sortd.thy (raw)
    • Sorted.thy (raw)
    • Sorti.thy (raw)
    • TestAllInd.thy (raw)
    • testc.thy (raw)
  • lbs-pres
    • hipster-sub.jpg (raw)
    • hipster-sub.odg (raw)
    • hipster-sub.svg (raw)
    • induct-schemes-tac.html (raw)
    • tegu.html (raw)
    • umbrella-s.gif (raw)
  • tthhp
    • bench.png (raw)
    • bench.tiff (raw)
    • comp.png (raw)
    • comp.tiff (raw)
    • hipster-sub.jpg (raw)
    • hipster-sub.odg (raw)
    • hipster-sub.svg (raw)
    • induct-schemes-tac.html (raw)
    • rec-ind-hipster.html (raw)
    • tegu.html (raw)
    • umbrella-s.gif (raw)
  • WAIT-pres
    • hipster-sub.jpg (raw)
    • hipster-sub.odg (raw)
    • hipster-sub.svg (raw)
    • induct-schemes-tac.html (raw)
    • tegu.html (raw)
    • umbrella-s.gif (raw)
• TestTheories
  • BinTree.thy (raw)
  • Listing.thy (raw)
  • Listi.thy (raw)
  • Merge.thy (raw)
  • Naturals.thy (raw)
  • NewDat.thy (raw)
  • Sorting.thy (raw)
  • SortM.thy (raw)
  • testI.thy (raw)
  • Turtle.thy (raw)
  • expl-cases
    • addMul.thy (raw)
    • dump.txt (raw)
    • lezpAdd.thy (raw)
  • List-prfs
    • BasicL.thy (raw)
    • HardL.thy (raw)
    • MediumL.thy (raw)
    • out-T.txt (raw)
    • Pals.thy (raw)
    • Sorted.thy (raw)
    • Test.thy (raw)
  • Nat-prfs
    • DefNats.thy (raw)
    • ProofN.thy (raw)