Mercurial
isabelle
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
branches
|
file
| revisions |
annotate
|
diff
|
rss
src/HOL/List.ML
2000-02-24
nipkow
2000-02-24
Added and renamed a lemma.
file
|
diff
|
annotate
2000-02-18
paulson
2000-02-18
expandshort
file
|
diff
|
annotate
2000-01-26
nipkow
2000-01-26
optimized xs[i:=x]!j lemmas.
file
|
diff
|
annotate
2000-01-12
nipkow
2000-01-12
More lemmas.
file
|
diff
|
annotate
2000-01-10
nipkow
2000-01-10
Forgot to "call" MicroJava in makefile. Added list_all2 to List.
file
|
diff
|
annotate
1999-12-13
paulson
1999-12-13
expandshort
file
|
diff
|
annotate
1999-11-11
nipkow
1999-11-11
Imported Conny's lemmas from MicroJava
file
|
diff
|
annotate
1999-09-21
nipkow
1999-09-21
Mod because of new solver interface.
file
|
diff
|
annotate
1999-08-18
nipkow
1999-08-18
Added take_all and drop_all to simpset.
file
|
diff
|
annotate
1999-08-16
wenzelm
1999-08-16
'a list: Nil, Cons;
file
|
diff
|
annotate
1999-07-19
paulson
1999-07-19
NatBin: binary arithmetic for the naturals
file
|
diff
|
annotate
1999-07-18
nipkow
1999-07-18
Modifid length_tl
file
|
diff
|
annotate
1999-06-17
paulson
1999-06-17
expandshort
file
|
diff
|
annotate
1999-06-11
nipkow
1999-06-11
rev=rev lemma.
file
|
diff
|
annotate
1999-06-10
paulson
1999-06-10
many new lemmas about take & drop, incl the famous take-lemma Ran expandshort
file
|
diff
|
annotate
1999-06-07
nipkow
1999-06-07
Added lots of 'replicate' lemmas.
file
|
diff
|
annotate
1999-04-20
paulson
1999-04-20
tidied
file
|
diff
|
annotate
1999-04-15
nipkow
1999-04-15
Added new thms.
file
|
diff
|
annotate
1999-04-01
pusch
1999-04-01
new definition for nth. added warnings, if primrec definition is deleted from simpset.
file
|
diff
|
annotate
1999-03-17
wenzelm
1999-03-17
Theory.sign_of;
file
|
diff
|
annotate
1999-03-08
nipkow
1999-03-08
modified zip
file
|
diff
|
annotate
1999-01-29
paulson
1999-01-29
expandshort
file
|
diff
|
annotate
1999-01-19
paulson
1999-01-19
removal of the (thm list) argument of mk_cases
file
|
diff
|
annotate
1999-01-09
nipkow
1999-01-09
Refined arith tactic.
file
|
diff
|
annotate
1999-01-04
nipkow
1999-01-04
Shortened a proof.
file
|
diff
|
annotate
1999-01-04
nipkow
1999-01-04
Version 1.0 of linear nat arithmetic.
file
|
diff
|
annotate
1998-11-27
nipkow
1998-11-27
At last: linear arithmetic for nat!
file
|
diff
|
annotate
1998-10-23
oheimb
1998-10-23
corrected auto_tac (applications of unsafe wrappers)
file
|
diff
|
annotate
1998-10-14
nipkow
1998-10-14
Nat: added zero_neq_conv List: added nth/update lemmas.
file
|
diff
|
annotate
1998-10-13
paulson
1998-10-13
length_Suc_conv is no longer given to AddIffs
file
|
diff
|
annotate
1998-09-23
paulson
1998-09-23
deleted needless parentheses
file
|
diff
|
annotate
1998-09-21
oheimb
1998-09-21
re-added mem and list_all
file
|
diff
|
annotate
1998-09-10
paulson
1998-09-10
in_set_butlast_appendI supersedes in_set_butlast_appendI1,2
file
|
diff
|
annotate
1998-09-09
oheimb
1998-09-09
changed constants mem and list_all to mere translations added filter_is_subset
file
|
diff
|
annotate
1998-09-04
nipkow
1998-09-04
Arith: less_diff_conv List: [i..j]
file
|
diff
|
annotate
1998-09-02
nipkow
1998-09-02
Added function upto to List. Had to rearrange loading sequence because now List uses Recdef.
file
|
diff
|
annotate
1998-08-20
paulson
1998-08-20
tidied
file
|
diff
|
annotate
1998-08-14
paulson
1998-08-14
expandshort
file
|
diff
|
annotate
1998-08-13
paulson
1998-08-13
even more tidying of Goal commands
file
|
diff
|
annotate
1998-08-12
oheimb
1998-08-12
added length_Suc_conv, finite_set
file
|
diff
|
annotate
1998-08-10
nipkow
1998-08-10
More lemmas about lex.
file
|
diff
|
annotate
1998-08-08
nipkow
1998-08-08
List now contains some lexicographic orderings.
file
|
diff
|
annotate
1998-08-06
paulson
1998-08-06
even more tidying of Goal commands
file
|
diff
|
annotate
1998-08-06
nipkow
1998-08-06
New lemmas in List and Lambda in IsaMakefile
file
|
diff
|
annotate
1998-07-27
nipkow
1998-07-27
conversion bug in simpproc list_eq
file
|
diff
|
annotate
1998-07-24
berghofe
1998-07-24
Adapted to new datatype package.
file
|
diff
|
annotate
1998-07-20
nipkow
1998-07-20
Added simproc list_eq.
file
|
diff
|
annotate
1998-07-12
wenzelm
1998-07-12
isatool expandshort;
file
|
diff
|
annotate
1998-07-06
nipkow
1998-07-06
Converted to Auto_tac
file
|
diff
|
annotate
1998-07-03
wenzelm
1998-07-03
removed duplicate thms;
file
|
diff
|
annotate
1998-06-24
nipkow
1998-06-24
* HOL/List: new function list_update written xs[i:=v] that updates the i-th list position. May also be iterated as in xs[i:=a,j:=b,...].
file
|
diff
|
annotate
1998-06-17
nipkow
1998-06-17
goal -> Goal
file
|
diff
|
annotate
1998-05-18
nipkow
1998-05-18
Cleaned up and simplified etc. snoc_induct/exhaust -> rev_induct_exhaust.
file
|
diff
|
annotate
1998-05-12
nipkow
1998-05-12
Removed duplicate list_length_induct
file
|
diff
|
annotate
1998-04-27
nipkow
1998-04-27
Added a few lemmas. Renamed expand_const -> split_const.
file
|
diff
|
annotate
1998-03-07
nipkow
1998-03-07
Removed `addsplits [expand_if]'
file
|
diff
|
annotate
1998-03-06
nipkow
1998-03-06
expand_if is now by default part of the simpset.
file
|
diff
|
annotate
1998-02-24
nipkow
1998-02-24
Added some lemmas.
file
|
diff
|
annotate
1998-02-22
nipkow
1998-02-22
New induction schemas for lists (length and snoc).
file
|
diff
|
annotate
1998-02-12
wenzelm
1998-02-12
*** empty log message ***
file
|
diff
|
annotate