Commits · 5e3bd0e687a82dbaaaedb29cbddd741f985e6f2e · Why3 / why3

15 Jan, 2013 1 commit
- rename 0.95-dev to 0.95 in the proof sessions · 5e3bd0e6
  Andrei Paskevich authored Jan 15, 2013
  
  5e3bd0e6
14 Jan, 2013 1 commit
- vstte10_queens: removed a lemma · 0ff0abb1
  Jean-Christophe Filliâtre authored Jan 14, 2013
  
  0ff0abb1
13 Jan, 2013 2 commits
- tower_of_hanoi: update session file · 05cb56dc
  Andrei Paskevich authored Jan 13, 2013
  
  05cb56dc
- tower of hanoi: coq proofs · deab494e
  Andrei Paskevich authored Jan 13, 2013
```
generic theories can be moved to theories/list.why
```
  deab494e
11 Jan, 2013 1 commit
- slightly generalized Tower of Hanoi (two Coq lemmas not proved yet) · c0c54f6b
  Andrei Paskevich authored Jan 11, 2013
  
  c0c54f6b
10 Jan, 2013 4 commits
- minor fix · 3b6e790c
  Andrei Paskevich authored Jan 10, 2013
  
  3b6e790c
- a simpler coqless version of the Hanoi Tower · 3cf23683
  Andrei Paskevich authored Jan 10, 2013
  
  3cf23683
- slight simplification of mjrty example using a new module array.NumOfEq · a0a10793
  Jean-Christophe Filliâtre authored Jan 10, 2013
  
  a0a10793
- Update Coq proof for queens.mlw:t3.3.12.1.4. · 5184e595
  Guillaume Melquiond authored Jan 10, 2013
  
  5184e595
07 Jan, 2013 2 commits
- tower of hanoi: proof completed (apart from lemmas on lists) · 2e592dc1
  Jean-Christophe Filliâtre authored Jan 07, 2013
  
  2e592dc1
- fixed hypothesis 4 · ae4fe168
  MARCHE Claude authored Dec 21, 2012
  
  ae4fe168
21 Dec, 2012 1 commit
- new example: tower of Hanoi (in progress) · e8361058
  Jean-Christophe Filliâtre authored Dec 21, 2012
  
  e8361058
04 Dec, 2012 1 commit
- Update examples due to the new Coq realization for map.Map. · 7c701a30
  Guillaume Melquiond authored Dec 04, 2012
  
  7c701a30
23 Nov, 2012 1 commit
- fm 2012 pbm 3: simplification · 9b988654
  Jean-Christophe Filliâtre authored Nov 23, 2012
  
  9b988654
21 Nov, 2012 3 commits
- fm 2012 pbm 3: simplification · 2f85be2b
  Jean-Christophe Filliâtre authored Nov 21, 2012
  
  2f85be2b
- fm 2012, pbm 3 (spec simplification) · e58be120
  Jean-Christophe Filliâtre authored Nov 21, 2012
  
  e58be120
- fm 2012, pbm 3 (in progress) · cd95bfe1
  Jean-Christophe Filliâtre authored Nov 21, 2012
  
  cd95bfe1
19 Nov, 2012 1 commit
- fm 2012, pbm 3 (in progress) · 804f893a
  Jean-Christophe Filliâtre authored Nov 19, 2012
  
  804f893a
12 Nov, 2012 1 commit
- Ensure radix-2 and radix-8 constants are properly sent to Gappa. · 33f16ba1
  Guillaume Melquiond authored Nov 12, 2012
  
  33f16ba1
09 Nov, 2012 2 commits
- building a theory using the API, documented · bbdcd12d
  MARCHE Claude authored Nov 09, 2012
  
  bbdcd12d
- example of use of Session API · d0eced69
  MARCHE Claude authored Nov 09, 2012
  
  d0eced69
07 Nov, 2012 1 commit
- fix parsing of hex reals · d926138c
  Andrei Paskevich authored Nov 07, 2012
  
  d926138c
05 Nov, 2012 2 commits
- update session for edit_distance on moloch · a13953ad
  MARCHE Claude authored Nov 05, 2012
  
  a13953ad
- Fix proofs after modified wp of "for ... downto" · 55b5cc61
  MARCHE Claude authored Nov 05, 2012
  
  55b5cc61
04 Nov, 2012 1 commit
- core/Term: smart, protecting constructors for integer constants · 16692122
  MARCHE Claude authored Nov 04, 2012
  
  16692122
03 Nov, 2012 1 commit
- dijkstra: updated proof on moloch · 5dce6207
  Jean-Christophe Filliâtre authored Nov 03, 2012
  
  5dce6207
02 Nov, 2012 3 commits
- dijkstra: proof completed · 878754c5
  Jean-Christophe Filliâtre authored Nov 02, 2012
  
  878754c5
- updated proof of vstte12_bfs · 7c252cb1
  Jean-Christophe Filliâtre authored Nov 02, 2012
  
  7c252cb1
- example Dijkstra: proof in progress · 0203ede7
  Jean-Christophe Filliâtre authored Nov 02, 2012
  
  0203ede7
31 Oct, 2012 8 commits
- distance -> optimal_replay · 205f6b86
  Jean-Christophe Filliâtre authored Oct 31, 2012
  
  205f6b86
- vacid_0_sparse_array_2 -> vacid_0_sparse_array · 481ac0c5
  Jean-Christophe Filliâtre authored Oct 31, 2012
  
  481ac0c5
- vstte12_ring_buffer_2 -> vstte12_ring_buffer · 0ba85a84
  Jean-Christophe Filliâtre authored Oct 31, 2012
  
  0ba85a84
- why3doc: fixed colors · 184f6472
  Jean-Christophe Filliâtre authored Oct 31, 2012
  
  184f6472
- use DTD on the Why3 web page · 4adc9ac4
  MARCHE Claude authored Oct 31, 2012
  
  4adc9ac4
- updated sessions after fixing the name of subgoals · 2d8a7f6b
  MARCHE Claude authored Oct 31, 2012
  
  2d8a7f6b
- update sessions with new explanations · 6e1e49a8
  MARCHE Claude authored Oct 31, 2012
  
  6e1e49a8
- update CHANGES · c3842ce2
  MARCHE Claude authored Oct 31, 2012
  
  c3842ce2
30 Oct, 2012 3 commits
- change explanation for the VC of a whole function (no more "parameter") · e4e2cc81
  MARCHE Claude authored Oct 30, 2012
  
  e4e2cc81
- update sessions · c9c143de
  Andrei Paskevich authored Oct 30, 2012
  
  c9c143de
- no implicit match in type invariants for records · 7e80633b
  Andrei Paskevich authored Oct 30, 2012
```
+ the implicitly bound variable in type invariants
  is now called "self"
```
  7e80633b