#
2e9b712b |
|
13-Feb-2020 |
nipkow <none@none> |
added lemmas
|
#
12a80644 |
|
10-Feb-2020 |
paulson <lp15@cam.ac.uk> |
some lemmas about the lex ordering on lists, etc.
|
#
32c7b8a2 |
|
09-Feb-2020 |
haftmann <none@none> |
more lemmas
|
#
0c4f403a |
|
27-Jan-2020 |
paulson <lp15@cam.ac.uk> |
A few lemmas connected with orderings
|
#
043c3b16 |
|
18-Jan-2020 |
traytel <none@none> |
new examples of BNF lifting across quotients using a new theory of confluence, which simplifies the relator subdistributivity proof obligation (a few new useful notions were added to HOL; notably the symmetric and equivalence closures of a relation)
|
#
a6ddae93 |
|
19-Oct-2019 |
haftmann <none@none> |
more lemmas
|
#
4ca08479 |
|
30-May-2019 |
nipkow <none@none> |
tuned proof
|
#
07bb9dfb |
|
21-May-2019 |
nipkow <none@none> |
strengthened lemma
|
#
fe03936a |
|
01-May-2019 |
haftmann <none@none> |
more lemmas --HG-- extra : rebase_source : 3e2ac977160873ea4b0f5fb90c505d1a2c674b91
|
#
3ef6740f |
|
18-Apr-2019 |
haftmann <none@none> |
incorporated various material from the AFP into the distribution --HG-- extra : rebase_source : 5e560f26b11abb81e42f7e18947eaa6c0d2e5837
|
#
9bbb928f |
|
28-Feb-2019 |
wenzelm <none@none> |
tuned proofs -- eliminated odd case_tac;
|
#
083015db |
|
21-Jan-2019 |
paulson <lp15@cam.ac.uk> |
new material about summations and powers, along with some tweaks
|
#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
26e81017 |
|
27-Nov-2018 |
wenzelm <none@none> |
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups; tuned signature;
|
#
ca7063ef |
|
18-Nov-2018 |
nipkow <none@none> |
added and tuned lemmas
|
#
e01498ae |
|
10-Nov-2018 |
haftmann <none@none> |
replaced some ancient ASCII syntax
|
#
ec8d5b30 |
|
10-Nov-2018 |
haftmann <none@none> |
clarified status of legacy input abbreviations
|
#
7800a6e6 |
|
31-Oct-2018 |
wenzelm <none@none> |
tuned;
|
#
7ac0b980 |
|
28-Oct-2018 |
nipkow <none@none> |
added lemmas
|
#
1ad5ed72 |
|
11-Oct-2018 |
nipkow <none@none> |
added simp-lemma
|
#
5dd0cee6 |
|
08-Oct-2018 |
nipkow <none@none> |
added simp-lemma
|
#
708adf55 |
|
05-Oct-2018 |
nipkow <none@none> |
more [simp]
|
#
9e188bc2 |
|
03-Oct-2018 |
nipkow <none@none> |
shuffle -> shuffles
|
#
17b7392c |
|
29-Sep-2018 |
nipkow <none@none> |
avoid confusing precedences
|
#
35f25e17 |
|
26-Sep-2018 |
nipkow <none@none> |
simpler def
|
#
23d0d04e |
|
11-Sep-2018 |
paulson <lp15@cam.ac.uk> |
A few new results, elimination of duplicates and more use of "pairwise"
|
#
367ce60b |
|
21-Aug-2018 |
haftmann <none@none> |
tuned whitespace --HG-- extra : rebase_source : 709c3ecd12d88f399349a5ad01c12f6828116fea
|
#
90811e7e |
|
20-Aug-2018 |
haftmann <none@none> |
removed ineffective code declarations
|
#
5167deb0 |
|
04-Aug-2018 |
wenzelm <none@none> |
recovered HOL-Proofs-Lambda from 8aedca31957d: avoid problems with program extraction according to d136af442665;
|
#
4a0d1115 |
|
03-Aug-2018 |
paulson <lp15@cam.ac.uk> |
de-applying
|
#
ee39c2af |
|
01-Aug-2018 |
paulson <lp15@cam.ac.uk> |
de-applying
|
#
bf3ad9bc |
|
17-Jul-2018 |
paulson <lp15@cam.ac.uk> |
more de-applying
|
#
a0960b42 |
|
28-Jun-2018 |
paulson <lp15@cam.ac.uk> |
Generalising and renaming some basic results
|
#
9ca3a517 |
|
03-Jun-2018 |
nipkow <none@none> |
allow tuple patterns in list comprehensions
|
#
a2458978 |
|
30-May-2018 |
nipkow <none@none> |
unused
|
#
e0e22efa |
|
22-May-2018 |
nipkow <none@none> |
First step to remove nonstandard "[x <- xs. P]" syntax: only input --HG-- extra : amend_source : a2e6a2312b63a5ed1947d3302e43341c073c9f03
|
#
b4145dfe |
|
19-May-2018 |
nipkow <none@none> |
added lemmas
|
#
c4d72a4c |
|
15-May-2018 |
nipkow <none@none> |
removed duplicates
|
#
b45a7d58 |
|
15-May-2018 |
nipkow <none@none> |
added lemmas
|
#
352f14bd |
|
14-May-2018 |
nipkow <none@none> |
cleaning up sorted
|
#
7f7d79b0 |
|
14-May-2018 |
nipkow <none@none> |
more sorted cleaning
|
#
6882225f |
|
14-May-2018 |
nipkow <none@none> |
cleaning up sorted
|
#
ff1ba275 |
|
13-May-2018 |
nipkow <none@none> |
mv lemma
|
#
74f263cb |
|
12-May-2018 |
nipkow <none@none> |
added lemmas
|
#
455d2918 |
|
10-May-2018 |
nipkow <none@none> |
more lemmas
|
#
dd96656d |
|
08-May-2018 |
nipkow <none@none> |
announce sorted changes
|
#
f3f05aca |
|
08-May-2018 |
nipkow <none@none> |
more efficient code
|
#
554c901e |
|
07-May-2018 |
nipkow <none@none> |
more "sorted" changes
|
#
d6194b67 |
|
08-May-2018 |
nipkow <none@none> |
new def of sorted and sorted_wrt --HG-- extra : amend_source : 063fe8412a72415725783d8336fe89d3cd0ca676
|
#
0fa1dc1a |
|
06-May-2018 |
nipkow <none@none> |
reinstated old lemma name
|
#
bdd8666f |
|
06-May-2018 |
nipkow <none@none> |
removed asm "finite"
|
#
3a4a7136 |
|
24-Apr-2018 |
haftmann <none@none> |
proper datatype for 8-bit characters
|
#
f801729e |
|
13-Apr-2018 |
nipkow <none@none> |
added lemma
|
#
2b9abbd8 |
|
26-Mar-2018 |
nipkow <none@none> |
added lemmas
|
#
e28ad6d3 |
|
24-Mar-2018 |
nipkow <none@none> |
added lemma
|
#
f5c4fc86 |
|
24-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
#
724da00d |
|
22-Feb-2018 |
nipkow <none@none> |
simplified def of stable
|
#
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
#
fd245e45 |
|
12-Feb-2018 |
nipkow <none@none> |
added lemmas
|
#
3dc755a5 |
|
21-Jan-2018 |
nipkow <none@none> |
made sorted fun again
|
#
b9ca1f27 |
|
20-Jan-2018 |
nipkow <none@none> |
imported patch sorted
|
#
0173f2e6 |
|
20-Jan-2018 |
bulwahn <none@none> |
add lemma on lists from Falling_Factorial_Sum entry
|
#
5385dbfa |
|
16-Jan-2018 |
wenzelm <none@none> |
standardized towards new-style formal comments: isabelle update_comments;
|
#
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
#
2bcd91d0 |
|
13-Dec-2017 |
nipkow <none@none> |
added lemmas
|
#
af426f8d |
|
13-Dec-2017 |
nipkow <none@none> |
added min_list and arg_min_list
|
#
92d5e4db |
|
13-Dec-2017 |
nipkow <none@none> |
added lemmas
|
#
21dd3e2b |
|
04-Dec-2017 |
nipkow <none@none> |
more lemmas
|
#
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
#
a844fd17 |
|
21-Nov-2017 |
nipkow <none@none> |
more lemmas
|
#
8cb7d5f5 |
|
23-Oct-2017 |
nipkow <none@none> |
added lemma
|
#
4b9f5532 |
|
21-Oct-2017 |
bulwahn <none@none> |
remove trailing whitespaces in List
|
#
39370fc8 |
|
21-Oct-2017 |
bulwahn <none@none> |
drop a superfluous assumption that was found by the find_unused_assms command
|
#
6cd6c516 |
|
21-Oct-2017 |
bulwahn <none@none> |
drop a superfluous assumption that was found by the find_unused_assms command and tune proof
|
#
d603bdb5 |
|
21-Oct-2017 |
bulwahn <none@none> |
drop a superfluous assumption that was found by the find_unused_assms command and tune proof
|
#
8e29256b |
|
16-Oct-2017 |
nipkow <none@none> |
added [simp]
|
#
f2f0903b |
|
13-Oct-2017 |
nipkow <none@none> |
added lemmas, tuned spaces
|
#
203fe9aa |
|
11-Oct-2017 |
nipkow <none@none> |
relaxed assm
|
#
eda74618 |
|
09-Oct-2017 |
haftmann <none@none> |
tuned imports --HG-- extra : rebase_source : bc9797cb892085195c2d8662a7ca3896dd1e5011
|
#
1e77e2ad |
|
14-Sep-2017 |
nipkow <none@none> |
two new simp rules
|
#
68689081 |
|
14-Sep-2017 |
nipkow <none@none> |
added lemma
|
#
3fdf21c1 |
|
13-Sep-2017 |
nipkow <none@none> |
added lemma; zip_with -> map2
|
#
7a12337e |
|
12-Sep-2017 |
nipkow <none@none> |
introduced zip_with
|
#
02021a5d |
|
11-Sep-2017 |
nipkow <none@none> |
added lemma
|
#
90e3ae3c |
|
01-Sep-2017 |
bulwahn <none@none> |
more facts on Map.map_of and List.zip --HG-- extra : rebase_source : aabab8a4de88b4f4ff69c542f7e9d1c239fc1a0f
|
#
7bd724e7 |
|
29-Aug-2017 |
eberlm <eberlm@in.tum.de> |
Some small lemmas about polynomials and FPSs --HG-- extra : rebase_source : b31b5bb1a9508cf7149022396f1a2b51a88c8dc9
|
#
5a17ac10 |
|
25-Aug-2017 |
nipkow <none@none> |
Added lemmas
|
#
3773efc1 |
|
16-Aug-2017 |
nipkow <none@none> |
added lemma
|
#
c7fc4ed4 |
|
16-Aug-2017 |
nipkow <none@none> |
more reorganization around sorted_wrt
|
#
e736333f |
|
15-Aug-2017 |
nipkow <none@none> |
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
|
#
65953a85 |
|
06-Aug-2017 |
bulwahn <none@none> |
slightly generalized card_lists_distinct_length_eq; renamed specialized card_lists_distinct_length_eq to card_lists_distinct_length_eq'; tuned
|
#
f90e5a66 |
|
08-Jul-2017 |
nipkow <none@none> |
revised lemma
|
#
4c6c4317 |
|
08-Jul-2017 |
nipkow <none@none> |
generalized lemma
|
#
6f4327d5 |
|
07-Jul-2017 |
nipkow <none@none> |
added lemma
|
#
e0d246a1 |
|
29-May-2017 |
eberlm <eberlm@in.tum.de> |
reorganised material on sublists --HG-- rename : src/HOL/Library/Sublist_Order.thy => src/HOL/Library/Subseq_Order.thy extra : amend_source : e295fcfca4d0d9db4c5591741cb62b62bb340c87
|
#
bc83a162 |
|
03-Apr-2017 |
eberlm <eberlm@in.tum.de> |
added shuffle product to HOL/List --HG-- extra : amend_source : f69971cd7b125b625e2945b41373d36d943083aa
|
#
229f8947 |
|
29-Jan-2017 |
wenzelm <none@none> |
added inj_def (redundant, analogous to surj_def, bij_def); tuned proofs;
|
#
2924ceb9 |
|
29-Jan-2017 |
wenzelm <none@none> |
tuned whitespace;
|
#
817fee61 |
|
12-Jan-2017 |
blanchet <none@none> |
added lemma
|
#
593ff4b4 |
|
17-Oct-2016 |
nipkow <none@none> |
setprod -> prod
|
#
351cc2e6 |
|
17-Oct-2016 |
nipkow <none@none> |
setsum -> sum
|
#
ad00661e |
|
16-Sep-2016 |
wenzelm <none@none> |
more symbols;
|
#
9147221e |
|
10-Sep-2016 |
wenzelm <none@none> |
tuned proofs;
|
#
a82bddb0 |
|
24-Aug-2016 |
nipkow <none@none> |
added lemma
|
#
28f73979 |
|
10-Aug-2016 |
haftmann <none@none> |
lists form a monoid --HG-- extra : rebase_source : 77a5f131b508e3b830e862b73e440f223ae25e1e
|
#
65b76842 |
|
29-Jul-2016 |
Andreas Lochbihler <none@none> |
add lemmas contributed by Peter Gammie
|
#
14001a0d |
|
22-Jul-2016 |
wenzelm <none@none> |
tuned proofs -- avoid unstructured calculation;
|
#
d25345da |
|
19-Jul-2016 |
Lars Hupel <lars.hupel@mytum.de> |
added missing transfer rule
|
#
0f0a91d1 |
|
02-Jul-2016 |
haftmann <none@none> |
more theorems
|
#
48473ab7 |
|
22-Jun-2016 |
wenzelm <none@none> |
bundle lifting_syntax;
|
#
1e23b491 |
|
16-Jun-2016 |
eberlm <none@none> |
Various additions to polynomials, FPSs, Gamma function
|
#
b073e135 |
|
29-May-2016 |
nipkow <none@none> |
added subtheory of longest common prefix
|
#
ddacf0c0 |
|
25-May-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
94ba250a |
|
17-May-2016 |
eberlm <none@none> |
Moved material from AFP/Randomised_Social_Choice to distribution
|
#
1daf8189 |
|
13-May-2016 |
wenzelm <none@none> |
eliminated use of empty "assms";
|
#
a2bc0021 |
|
25-Apr-2016 |
wenzelm <none@none> |
eliminated old 'def'; tuned comments;
|
#
f318340b |
|
09-Mar-2016 |
haftmann <none@none> |
moved
|
#
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
#
6688eecc |
|
17-Feb-2016 |
haftmann <none@none> |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
#
ef2cc6c5 |
|
17-Feb-2016 |
traytel <none@none> |
call the predicator of list list_all
|
#
e64e636d |
|
13-Jan-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
f1382dd6 |
|
08-Jan-2016 |
nipkow <none@none> |
added lemma
|
#
4216bc36 |
|
07-Jan-2016 |
wenzelm <none@none> |
more uniform treatment of package internals;
|
#
8e9ae40e |
|
05-Jan-2016 |
eberlm <none@none> |
Added some facts about polynomials
|
#
0bfb73b6 |
|
28-Dec-2015 |
wenzelm <none@none> |
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
|
#
c9f3da2d |
|
27-Dec-2015 |
wenzelm <none@none> |
discontinued ASCII replacement syntax <->;
|
#
6820dd05 |
|
10-Dec-2015 |
paulson <lp15@cam.ac.uk> |
not_leE -> not_le_imp_less and other tidying
|
#
0df376fc |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
ba84f220 |
|
18-Nov-2015 |
paulson <lp15@cam.ac.uk> |
New theorems mostly from Peter Gammie
|
#
2ceb4cc9 |
|
14-Nov-2015 |
wenzelm <none@none> |
option "inductive_defs" controls exposure of def and mono facts;
|
#
c79c7fe1 |
|
14-Nov-2015 |
haftmann <none@none> |
reverted half-baken 7d1127ac2251 --HG-- extra : rebase_source : 457832304889dc2d80d98b8be1a7e19764f1c9dc
|
#
3487f527 |
|
11-Nov-2015 |
Andreas Lochbihler <none@none> |
add various lemmas
|
#
be9ace2b |
|
09-Nov-2015 |
wenzelm <none@none> |
qualifier is mandatory by default;
|
#
8e8b881c |
|
04-Nov-2015 |
ballarin <none@none> |
Keyword 'rewrites' identifies rewrite morphisms.
|
#
71a6f397 |
|
17-Oct-2015 |
haftmann <none@none> |
code abbreviation for mapping over a fixed range --HG-- extra : rebase_source : ede20bd4497dbc9d290639d6c1abf8960f621d90
|
#
607ae3e3 |
|
09-Oct-2015 |
wenzelm <none@none> |
discontinued specific HTML syntax;
|
#
5012105f |
|
13-Sep-2015 |
wenzelm <none@none> |
tuned proofs -- less legacy;
|
#
85ed9565 |
|
01-Sep-2015 |
wenzelm <none@none> |
eliminated \<Colon>;
|
#
df44ab4c |
|
27-Aug-2015 |
haftmann <none@none> |
standardized some occurences of ancient "split" alias --HG-- extra : rebase_source : 706ba501d5c0596a2bde6e46d42aa8464a91ede5
|
#
bd18d479 |
|
27-Aug-2015 |
haftmann <none@none> |
more lemmas on sorting and multisets (due to Thomas Sewell) --HG-- extra : rebase_source : df9cf240f30d85ac4954aa584945beeef1d8de5c
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
62ae9c62 |
|
18-Jul-2015 |
wenzelm <none@none> |
prefer tactics with explicit context;
|
#
5b7d639c |
|
25-Jun-2015 |
wenzelm <none@none> |
tuned proofs;
|
#
77fe662c |
|
22-Jun-2015 |
nipkow <none@none> |
modernized name
|
#
4bd74eb0 |
|
30-Apr-2015 |
wenzelm <none@none> |
more formal source, more PIDE markup;
|
#
43ff03bf |
|
30-Apr-2015 |
wenzelm <none@none> |
tuned -- avoid odd rebinding of "ctxt" and "context";
|
#
ce141da1 |
|
30-Apr-2015 |
wenzelm <none@none> |
tuned;
|
#
cb57defc |
|
29-Apr-2015 |
wenzelm <none@none> |
tuned;
|
#
293b5ec0 |
|
17-Mar-2015 |
nipkow <none@none> |
added lemmas
|
#
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
#
d0f09b82 |
|
11-Feb-2015 |
Andreas Lochbihler <none@none> |
add parametricity rules for monotone, fun_lub, and fun_ord
|
#
c16f1f49 |
|
29-Dec-2014 |
wenzelm <none@none> |
tuned;
|
#
54210d9c |
|
11-Nov-2014 |
noschinl <none@none> |
added lemma
|
#
a650e386 |
|
10-Nov-2014 |
traytel <none@none> |
dropped redundant transfer rules (now proved and registered by datatype and plugins)
|
#
d6623f99 |
|
09-Nov-2014 |
wenzelm <none@none> |
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
|
#
23571538 |
|
07-Nov-2014 |
traytel <none@none> |
more complete fp_sugars for sum and prod; tuned; removed theorem duplicates; removed obsolete Lifting_{Option,Product,Sum} theories
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
2e544a83 |
|
28-Oct-2014 |
nipkow <none@none> |
removed useless lemmas
|
#
e3c99303 |
|
29-Oct-2014 |
nipkow <none@none> |
tuned layout and proofs
|
#
5fc26177 |
|
11-Sep-2014 |
blanchet <none@none> |
updated news
|
#
2dbc8141 |
|
09-Sep-2014 |
nipkow <none@none> |
enamed drop_Suc_conv_tl and nth_drop' to Cons_nth_drop_Suc
|
#
caa51abc |
|
06-Sep-2014 |
haftmann <none@none> |
added various facts
|
#
e01167f4 |
|
02-Sep-2014 |
traytel <none@none> |
silenced nonexhaustive primrec warnings
|
#
4a4ba20a |
|
24-Sep-2014 |
haftmann <none@none> |
added lemmas --HG-- extra : rebase_source : 9983f0122781b2719b4390818c18fedd04f9cbb5
|
#
d22c2cb6 |
|
31-Aug-2014 |
haftmann <none@none> |
separated listsum material
|
#
a318027a |
|
25-Aug-2014 |
nipkow <none@none> |
added lemmas
|
#
84985a9a |
|
06-Aug-2014 |
blanchet <none@none> |
no need for 'set_simps' now that 'datatype_new' generates the desired 'set' property
|
#
d419adf4 |
|
21-Jul-2014 |
Andreas Lochbihler <none@none> |
add parametricity lemmas
|
#
e33effae |
|
19-Jul-2014 |
haftmann <none@none> |
reverse induction over nonempty lists
|
#
afe401fb |
|
09-Jul-2014 |
nipkow <none@none> |
added lemmas
|
#
38907e37 |
|
05-Jul-2014 |
haftmann <none@none> |
prefer ac_simps collections over separate name bindings for add and mult
|
#
e46c07fd |
|
04-Jul-2014 |
haftmann <none@none> |
reduced name variants for assoc and commute on plus and mult
|
#
bf4e83d3 |
|
28-Jun-2014 |
haftmann <none@none> |
fact consolidation
|
#
e7c3d6c8 |
|
24-Jun-2014 |
Andreas Lochbihler <none@none> |
add lemma
|
#
bf47da1c |
|
12-Jun-2014 |
nipkow <none@none> |
added [simp]
|
#
4ad40712 |
|
12-Jun-2014 |
blanchet <none@none> |
reintroduced vital 'Thm.transfer'
|
#
d4fd6e53 |
|
11-Jun-2014 |
blanchet <none@none> |
reduces Sledgehammer dependencies
|
#
42cd340d |
|
10-Jun-2014 |
blanchet <none@none> |
changed syntax of map: and rel: arguments to BNF-based datatypes
|
#
ed20523b |
|
09-Jun-2014 |
blanchet <none@none> |
use 'where' clause for selector default value syntax
|
#
c8c9c1d7 |
|
09-Jun-2014 |
nipkow <none@none> |
added List.union
|
#
5a60fc1f |
|
29-May-2014 |
blanchet <none@none> |
tuned whitespace, to make datatype definitions slightly less intimidating
|
#
312f030c |
|
26-May-2014 |
blanchet <none@none> |
got rid of '=:' squiggly
|
#
7e79b6fc |
|
14-May-2014 |
nipkow <none@none> |
added lemma
|
#
7812dc7c |
|
29-Apr-2014 |
wenzelm <none@none> |
prefer plain ASCII / latex over not-so-universal Unicode;
|
#
0811cf40 |
|
23-Apr-2014 |
blanchet <none@none> |
move size hooks together, with new one preceding old one and sharing same theory data
|
#
d766ca99 |
|
12-Apr-2014 |
haftmann <none@none> |
more operations and lemmas --HG-- extra : rebase_source : 8f5be7e0cdc09c667e66c2cda2c667d4da6e5f73
|
#
ab2b75bb |
|
10-Apr-2014 |
kuncar <none@none> |
make list_all an abbreviation of pred_list - prevent duplication
|
#
85e48936 |
|
10-Apr-2014 |
kuncar <none@none> |
simplify and fix theories thanks to 356a5efdb278
|
#
15939e27 |
|
10-Apr-2014 |
kuncar <none@none> |
abstract Domainp in relator_domain rules => more natural statement of the rule
|
#
128e121b |
|
10-Apr-2014 |
kuncar <none@none> |
more appropriate name (Lifting.invariant -> eq_onp)
|
#
845456ae |
|
10-Apr-2014 |
kuncar <none@none> |
left_total and left_unique rules are now transfer rules (cleaner solution, reflexvity_rule attribute not needed anymore)
|
#
81d6c2a2 |
|
21-Mar-2014 |
wenzelm <none@none> |
more qualified names;
|
#
12157cd1 |
|
19-Mar-2014 |
haftmann <none@none> |
elongated INFI and SUPR, to reduced risk of confusing theorems names in the future while still being consistent with INTER and UNION
|
#
4f5ebd94 |
|
16-Mar-2014 |
haftmann <none@none> |
normalising simp rules for compound operators
|
#
3eabe156 |
|
13-Mar-2014 |
blanchet <none@none> |
killed a few 'metis' calls
|
#
b9ba5739 |
|
06-Mar-2014 |
blanchet <none@none> |
renamed 'fun_rel' to 'rel_fun'
|
#
e1814034 |
|
06-Mar-2014 |
blanchet <none@none> |
renamed 'prod_rel' to 'rel_prod'
|
#
da006ee0 |
|
06-Mar-2014 |
blanchet <none@none> |
renamed 'set_rel' to 'rel_set'
|
#
8f53ef93 |
|
06-Mar-2014 |
blanchet <none@none> |
renamed 'map_pair' to 'map_prod'
|
#
5ceaf5a7 |
|
28-Feb-2014 |
nipkow <none@none> |
added function "List.extract"
|
#
bbeeaf3d |
|
28-Feb-2014 |
traytel <none@none> |
load Metis a little later
|
#
dd44ffb4 |
|
20-Feb-2014 |
blanchet <none@none> |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
#
ce43d47f |
|
19-Feb-2014 |
blanchet <none@none> |
merged 'List.set' with BNF-generated 'set'
|
#
98e61750 |
|
18-Feb-2014 |
kuncar <none@none> |
delete or move now not necessary reflexivity rules due to 1726f46d2aa8
|
#
a1d385ea |
|
17-Feb-2014 |
blanchet <none@none> |
renamed 'datatype_new_compat' to 'datatype_compat'
|
#
e5a26553 |
|
16-Feb-2014 |
blanchet <none@none> |
folded 'rel_option' into 'option_rel'
|
#
2221ece4 |
|
16-Feb-2014 |
blanchet <none@none> |
folded 'list_all2' with the relator generated by 'datatype_new'
|
#
a96f0fee |
|
13-Feb-2014 |
blanchet <none@none> |
hide 'rel' name -- this one is waiting to be merged with 'list_all2'
|
#
2f0985b8 |
|
13-Feb-2014 |
blanchet <none@none> |
renamed 'enriched_type' to more informative 'functor' (following the renaming of enriched type constructors to bounded natural functors) --HG-- rename : src/HOL/Tools/enriched_type.ML => src/HOL/Tools/functor.ML
|
#
447c00c8 |
|
13-Feb-2014 |
blanchet <none@none> |
merged 'Option.map' and 'Option.map_option'
|
#
b21bf852 |
|
13-Feb-2014 |
blanchet <none@none> |
merged 'List.map' and 'List.list.map'
|
#
80ec2685 |
|
12-Feb-2014 |
blanchet <none@none> |
tuning
|
#
aff8c6a4 |
|
12-Feb-2014 |
blanchet <none@none> |
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'
|
#
40e0ba91 |
|
12-Feb-2014 |
blanchet <none@none> |
renamed 'nat_{case,rec}' to '{case,rec}_nat'
|
#
f7053da7 |
|
12-Feb-2014 |
blanchet <none@none> |
compatibility names
|
#
041d6368 |
|
12-Feb-2014 |
blanchet <none@none> |
use new selector support to define 'the', 'hd', 'tl'
|
#
0d093612 |
|
12-Feb-2014 |
blanchet <none@none> |
transformed 'option' and 'list' into new-style datatypes (but register them as old-style as well) * * * compile * * * tuned imports to prevent merge issues in 'Main'
|
#
290db6b4 |
|
25-Jan-2014 |
haftmann <none@none> |
avoid (now superfluous) indirect passing of constant names
|
#
9250249f |
|
25-Jan-2014 |
haftmann <none@none> |
prefer explicit code symbol type over ad-hoc name mangling
|
#
325c96bf |
|
24-Jan-2014 |
blanchet <none@none> |
killed 'More_BNFs' by moving its various bits where they (now) belong
|
#
e93b90ff |
|
31-Dec-2013 |
haftmann <none@none> |
fundamental treatment of undefined vs. universally partial replaces code_abort
|
#
9660f69e |
|
31-Dec-2013 |
haftmann <none@none> |
more abstract declaration of code attributes
|
#
13c9f359 |
|
27-Dec-2013 |
haftmann <none@none> |
prefer target-style syntaxx for sublocale
|
#
ac866a0f |
|
25-Dec-2013 |
haftmann <none@none> |
prefer more canonical names for lemmas on min/max
|
#
2a3ae7e6 |
|
27-Nov-2013 |
Andreas Lochbihler <none@none> |
remove junk
|
#
f55a6e4d |
|
21-Nov-2013 |
blanchet <none@none> |
rationalize imports
|
#
030bdef2 |
|
20-Nov-2013 |
Andreas Lochbihler <none@none> |
add predicate version of lexicographic order on lists
|
#
138816de |
|
19-Nov-2013 |
haftmann <none@none> |
eliminiated neg_numeral in favour of - (numeral _)
|
#
0f655efd |
|
18-Nov-2013 |
hoelzl <none@none> |
add lemmas Suc_funpow and id_funpow to simpset; add lemma map_add_upt --HG-- extra : rebase_source : 02e892232f20d46af3dd46c4047e264fc49d378b
|
#
2040f365 |
|
12-Nov-2013 |
blanchet <none@none> |
port list comprehension simproc to 'Ctr_Sugar' abstraction
|
#
ade011bf |
|
10-Nov-2013 |
haftmann <none@none> |
qualifed popular user space names
|
#
03633065 |
|
18-Oct-2013 |
blanchet <none@none> |
killed most "no_atp", to make Sledgehammer more complete
|
#
23931936 |
|
27-Sep-2013 |
nipkow <none@none> |
added code eqns for bounded LEAST operator
|
#
b0527b24 |
|
26-Sep-2013 |
lammich <lammich@in.tum.de> |
Added symmetric code_unfold-lemmas for null and is_none
|
#
7f378b77 |
|
18-Sep-2013 |
traytel <none@none> |
added two functions to List (one contributed by Manuel Eberl)
|
#
6aa030fc |
|
17-Sep-2013 |
nipkow <none@none> |
added and tuned lemmas
|
#
0866b3ef |
|
05-Sep-2013 |
traytel <none@none> |
list_to_set_comprehension: don't crash in case distinctions on datatypes with even number of constructors
|
#
7237bdd9 |
|
02-Sep-2013 |
wenzelm <none@none> |
tuned proofs -- clarified flow of facts wrt. calculation;
|
#
06329277 |
|
13-Aug-2013 |
wenzelm <none@none> |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
#
61e69372 |
|
13-Aug-2013 |
kuncar <none@none> |
move Lifting/Transfer relevant parts of Library/Quotient_* to Main
|
#
a7b3de52 |
|
23-Jun-2013 |
haftmann <none@none> |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier --HG-- extra : rebase_source : ff8027ac9606264aa4b2d4f8da037c426a3db98b
|
#
d820eec9 |
|
15-Jun-2013 |
haftmann <none@none> |
lifting for primitive definitions; explicit conversions from and to lists of coefficients, used for generated code; replaced recursion operator poly_rec by fold_coeffs, preferring function definitions for non-trivial recursions; prefer pre-existing gcd operation for gcd
|
#
1253431c |
|
15-Jun-2013 |
haftmann <none@none> |
selection operator smallest_prime_beyond
|
#
ffb245a6 |
|
25-May-2013 |
haftmann <none@none> |
weaker precendence of syntax for big intersection and union on sets
|
#
ffcd6989 |
|
25-May-2013 |
wenzelm <none@none> |
syntax translations always depend on context;
|
#
e712bb09 |
|
24-May-2013 |
wenzelm <none@none> |
tuned signature;
|
#
5ca6bbf3 |
|
23-May-2013 |
noschinl <none@none> |
more lemmas for sorted_list_of_set
|
#
edf89801 |
|
05-May-2013 |
nipkow <none@none> |
tail recursive version of map, for code generation, optionally
|
#
958e3b8f |
|
23-Apr-2013 |
haftmann <none@none> |
tuned: unnamed contexts, interpretation and sublocale in locale target; corrected slip in List.thy: setsum requires commmutativity
|
#
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
#
d6ca5a22 |
|
05-Apr-2013 |
traytel <none@none> |
allow redundant cases in the list comprehension translation
|
#
f1d51965 |
|
27-Mar-2013 |
haftmann <none@none> |
centralized various multiset operations in theory multiset; more conversions between multisets and lists respectively --HG-- extra : rebase_source : 93a1492ea9887e2bb60374621b48587c8a351c80
|
#
de37771f |
|
26-Mar-2013 |
haftmann <none@none> |
explicit sublocale dependency for Min/Max yields more appropriate Min/Max prefix for a couple of facts
|
#
d4cae3bf |
|
23-Mar-2013 |
haftmann <none@none> |
fundamental revision of big operators on sets
|
#
b7e15901 |
|
28-Feb-2013 |
wenzelm <none@none> |
provide common HOLogic.conj_conv and HOLogic.eq_conv;
|
#
6a841933 |
|
28-Feb-2013 |
wenzelm <none@none> |
just one HOLogic.Trueprop_conv, with regular exception CTERM; tuned;
|
#
3e0fffd8 |
|
24-Feb-2013 |
wenzelm <none@none> |
prefer stateless 'ML_val' for tests;
|
#
6b8e5a08 |
|
17-Feb-2013 |
haftmann <none@none> |
Sieve of Eratosthenes
|
#
ecc208fc |
|
17-Feb-2013 |
haftmann <none@none> |
simplified construction of upto_aux
|
#
8619f3a1 |
|
16-Feb-2013 |
nipkow <none@none> |
tail recursive code for function "upto"
|
#
963a5558 |
|
15-Feb-2013 |
haftmann <none@none> |
systematic conversions between nat and nibble/char; more uniform approaches to execute operations on nibble/char --HG-- extra : rebase_source : 982810ecce9e31070e2293715ed744c3b68ae21d
|
#
fa22b8b3 |
|
13-Feb-2013 |
haftmann <none@none> |
abandoned theory Plain --HG-- extra : rebase_source : 6f5a395a55e8879386d1f79ab252c6fc2aca7dc5
|
#
27fdd5a0 |
|
13-Feb-2013 |
haftmann <none@none> |
combinator List.those; simprule for case distinction on Option.map expression
|
#
67709574 |
|
22-Jan-2013 |
traytel <none@none> |
separate data used for case translation from the datatype package
|
#
d564436d |
|
22-Jan-2013 |
berghofe <none@none> |
case translations performed in a separate check phase (with adjustments by traytel)
|
#
ad2a0d5c |
|
14-Dec-2012 |
nipkow <none@none> |
unified layout of defs
|
#
caec7139 |
|
07-Dec-2012 |
wenzelm <none@none> |
avoid ML_file in large theory files to improve performance of dependency discovery of main HOL (approx. 1s CPU time) -- relevant for any application using it, e.g. small paper sessions;
|
#
c28854e5 |
|
20-Nov-2012 |
hoelzl <none@none> |
add Countable_Set theory
|
#
f03a7699 |
|
08-Nov-2012 |
bulwahn <none@none> |
adjusting proofs as the set_comprehension_pointfree simproc breaks some existing proofs
|
#
bbf74aa0 |
|
20-Oct-2012 |
haftmann <none@none> |
moved quite generic material from theory Enum to more appropriate places --HG-- extra : rebase_source : aada8b3ff46b715201e6ecbb53f390c25461ebd9
|
#
d9333ba5 |
|
19-Oct-2012 |
webertj <none@none> |
Renamed {left,right}_distrib to distrib_{right,left}.
|
#
ccac2d08 |
|
10-Oct-2012 |
Andreas Lochbihler <none@none> |
tail-recursive implementation for length
|
#
8f15c228 |
|
09-Oct-2012 |
kuncar <none@none> |
rename Set.project to Set.filter - more appropriate name
|
#
ff347444 |
|
07-Oct-2012 |
haftmann <none@none> |
consolidated names of theorems on composition; generalized former theorem UN_o; comp_assoc orients to the right, as is more common
|
#
e3227796 |
|
22-Aug-2012 |
wenzelm <none@none> |
prefer ML_file over old uses;
|
#
3f48b838 |
|
16-Aug-2012 |
haftmann <none@none> |
prefer eta-expanded code equations for fold, to accomodate tail recursion optimisation in Scala
|
#
4e7f72b3 |
|
31-Jul-2012 |
kuncar <none@none> |
more set operations expressed by Finite_Set.fold
|
#
8b5fa487 |
|
29-Apr-2012 |
bulwahn <none@none> |
making sorted_list_of_set executable
|
#
b3ff13a2 |
|
20-Apr-2012 |
huffman <none@none> |
strengthen rule list_all2_induct
|
#
8567704a |
|
06-Apr-2012 |
haftmann <none@none> |
abandoned almost redundant *_foldr lemmas
|
#
864691f8 |
|
06-Apr-2012 |
haftmann <none@none> |
tuned
|
#
19e3dfe6 |
|
06-Apr-2012 |
haftmann <none@none> |
no preference wrt. fold(l/r); prefer fold rather than foldr for iterating over lists in generated code
|
#
55e11b0d |
|
03-Apr-2012 |
griff <none@none> |
renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
|
#
559b5232 |
|
26-Mar-2012 |
nipkow <none@none> |
reverted to canonical name
|
#
4913081d |
|
26-Mar-2012 |
nipkow <none@none> |
Functions and lemmas by Christian Sternagel
|
#
8bb6233a |
|
25-Mar-2012 |
huffman <none@none> |
merged fork with new numeral representation (see NEWS)
|
#
a3193ed0 |
|
13-Mar-2012 |
wenzelm <none@none> |
tuned proofs -- eliminated pointless chaining of facts after 'interpret';
|
#
81c2aa38 |
|
12-Mar-2012 |
noschinl <none@none> |
tuned proofs
|
#
816f67f4 |
|
27-Feb-2012 |
nipkow <none@none> |
converting "set [...]" to "{...}" in evaluation results
|
#
559698a1 |
|
25-Feb-2012 |
bulwahn <none@none> |
one general list_all2_update_cong instead of two special ones
|
#
484c9d58 |
|
24-Feb-2012 |
haftmann <none@none> |
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy --HG-- extra : rebase_source : ed15629634477aff0a8efea30547f496c70907ad
|
#
37822d49 |
|
23-Feb-2012 |
haftmann <none@none> |
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
|
#
e247b6c3 |
|
16-Feb-2012 |
bulwahn <none@none> |
removing unnecessary premises in theorems of List theory
|
#
6223e7f6 |
|
10-Feb-2012 |
Cezary Kaliszyk <cezarykaliszyk@gmail.com> |
more specification of the quotient package in IsarRef
|
#
05782632 |
|
07-Feb-2012 |
blanchet <none@none> |
use 'primrec' to define "rotate1", for uniformity (and to help first-order tools that rely on "Spec_Rules")
|
#
bdc7d91c |
|
07-Feb-2012 |
blanchet <none@none> |
removed fact that confuses SPASS -- better rely on "rev_rev_ident", which is stronger and more ATP friendly
|
#
4721f705 |
|
05-Feb-2012 |
bulwahn <none@none> |
adding code equation for Relation.image; adding map_project as correspondence to map_filter on lists
|
#
bb75bf75 |
|
05-Feb-2012 |
bulwahn <none@none> |
another try to improve code generation of set equality (cf. da32cf32c0c7)
|
#
b34ad4bb |
|
02-Feb-2012 |
bulwahn <none@none> |
adding a minimally refined equality on sets for code generation
|
#
accb2370 |
|
31-Jan-2012 |
bulwahn <none@none> |
adding code equation for setsum
|
#
99b811bf |
|
23-Jan-2012 |
huffman <none@none> |
generalize type of List.listrel
|
#
f742e269 |
|
23-Jan-2012 |
bulwahn <none@none> |
adding code generation for some list relations
|
#
88064256 |
|
10-Jan-2012 |
berghofe <none@none> |
pred_subset/equals_eq are now standard pred_set_conv rules
|
#
12f40542 |
|
07-Jan-2012 |
haftmann <none@none> |
massaging of code setup for sets --HG-- extra : rebase_source : d88e8eabd9d4067b161ff0d4e077408f826712f8
|
#
1d7d5518 |
|
07-Jan-2012 |
haftmann <none@none> |
corrected slip
|
#
46deb113 |
|
07-Jan-2012 |
haftmann <none@none> |
restore convenient code_abbrev declarations (particulary important if List.set is not the formal constructor for sets)
|
#
2021be2d |
|
06-Jan-2012 |
haftmann <none@none> |
moved lemmas about List.set and set operations to List theory --HG-- extra : rebase_source : acbab180eefc1dba0e1ed3007e87bf7039ff4047
|
#
e90bcf54 |
|
06-Jan-2012 |
haftmann <none@none> |
farewell to theory More_List --HG-- extra : rebase_source : 1faf1250c2e2d8499bbb199b166580783121c606
|
#
39aa30ee |
|
06-Jan-2012 |
wenzelm <none@none> |
improved list comprehension syntax: more careful treatment of position constraints, which enables PIDE markup; tuned;
|
#
96b404d6 |
|
06-Jan-2012 |
haftmann <none@none> |
incorporated canonical fold combinator on lists into body of List theory; refactored passages on List.fold(l/r) --HG-- extra : rebase_source : 022f0a101d8cefadae578fbbd0c1fd8958d910af
|
#
9a1a0296 |
|
05-Jan-2012 |
wenzelm <none@none> |
improved case syntax: more careful treatment of position constraints, which enables PIDE markup; tuned;
|
#
e1a874c1 |
|
29-Dec-2011 |
haftmann <none@none> |
qualified Finite_Set.fold
|
#
b5c42758 |
|
29-Dec-2011 |
haftmann <none@none> |
attribute code_abbrev superseedes code_unfold_post; tuned text --HG-- extra : rebase_source : 151b02554e820ef4b9e8f43b9a53512fbfc0e053
|
#
a4ee4da3 |
|
27-Dec-2011 |
haftmann <none@none> |
dropped fact whose names clash with corresponding facts on canonical fold
|
#
66d3554f |
|
24-Dec-2011 |
haftmann <none@none> |
dropped obsolete lemma member_set
|
#
8721bbeb |
|
19-Dec-2011 |
noschinl <none@none> |
add lemmas
|
#
231120dd |
|
15-Dec-2011 |
wenzelm <none@none> |
clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
|
#
97893bbc |
|
13-Dec-2011 |
noschinl <none@none> |
added lemmas
|
#
137f9bde |
|
09-Dec-2011 |
huffman <none@none> |
add induction rule for list_all2
|
#
80fb18a4 |
|
08-Dec-2011 |
bulwahn <none@none> |
removing special code generator setup for hd and last function because this causes problems with quickcheck narrowing as the Haskell Prelude functions throw errors that cannot be caught instead of PatternFail exceptions
|
#
5ba926df |
|
01-Dec-2011 |
hoelzl <none@none> |
cardinality of sets of lists
|
#
a495a026 |
|
20-Nov-2011 |
wenzelm <none@none> |
eliminated obsolete "standard";
|
#
70a22ffd |
|
19-Oct-2011 |
bulwahn <none@none> |
removing old code generator setup for lists
|
#
cf1f0a48 |
|
03-Oct-2011 |
bulwahn <none@none> |
adding lemma to List library for executable equation of the (refl) transitive closure
|
#
15635718 |
|
13-Sep-2011 |
huffman <none@none> |
tuned proofs
|
#
04792839 |
|
12-Sep-2011 |
bulwahn <none@none> |
added lemma motivated by a more specific lemma in the AFP-KBPs theories
|
#
7e65ae14 |
|
14-Sep-2011 |
hoelzl <none@none> |
renamed Complete_Lattices lemmas, removed legacy names
|
#
ad9e459c |
|
11-Sep-2011 |
nipkow <none@none> |
new fastforce replacing fastsimp - less confusing name
|
#
1cb08f4d |
|
01-Sep-2011 |
blanchet <none@none> |
added two lemmas about "distinct" to help Sledgehammer
|
#
b0604aca |
|
30-Aug-2011 |
bulwahn <none@none> |
adding list_size_append (thanks to Rene Thiemann)
|
#
f1e8b14a |
|
30-Aug-2011 |
bulwahn <none@none> |
strengthening list_size_pointwise (thanks to Rene Thiemann)
|
#
6e5665ea |
|
02-Aug-2011 |
krauss <none@none> |
moved recdef package to HOL/Library/Old_Recdef.thy --HG-- rename : src/HOL/Recdef.thy => src/HOL/Library/Old_Recdef.thy
|
#
ae3eeacd |
|
29-Jun-2011 |
wenzelm <none@none> |
modernized some simproc setup;
|
#
57cde513 |
|
27-Jun-2011 |
krauss <none@none> |
new Datatype.info_of_constr with strict behaviour wrt. to overloaded constructors -- side effect: function package correctly identifies 0::int as a non-constructor; renamed old version to info_of_constr_permissive, reflecting its semantics
|
#
ec1196d6 |
|
09-Jun-2011 |
wenzelm <none@none> |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
#
180c955e |
|
20-May-2011 |
haftmann <none@none> |
names of fold_set locales resemble name of characteristic property more closely
|
#
9e6090fb |
|
14-May-2011 |
haftmann <none@none> |
use pointfree characterisation for fold_set locale
|
#
dfc6e37a |
|
09-May-2011 |
noschinl <none@none> |
add a lemma about commutative append to List.thy
|
#
c3965daf |
|
08-May-2011 |
noschinl <none@none> |
removed assumption from lemma List.take_add
|
#
eb27e462 |
|
19-Apr-2011 |
wenzelm <none@none> |
eliminated Codegen.mode in favour of explicit argument;
|
#
6d2612c8 |
|
16-Apr-2011 |
wenzelm <none@none> |
modernized structure Proof_Context;
|
#
e56c255d |
|
16-Apr-2011 |
wenzelm <none@none> |
prefer local name spaces; tuned signatures; tuned;
|
#
3aaf94cf |
|
06-Apr-2011 |
wenzelm <none@none> |
separate structure Term_Position; dismantled remains of structure Type_Ext;
|
#
b5dc26dd |
|
30-Mar-2011 |
wenzelm <none@none> |
actually check list comprehension examples;
|
#
581058cf |
|
28-Mar-2011 |
wenzelm <none@none> |
list comprehension: strip positions where the translation cannot handle them right now;
|
#
83094238 |
|
22-Mar-2011 |
wenzelm <none@none> |
more selective strip_positions in case patterns -- reactivate translations based on "case _ of _" in HOL and special patterns in HOLCF;
|
#
6e39ef12 |
|
15-Mar-2011 |
nipkow <none@none> |
added lemma
|
#
8cd59bdd |
|
25-Feb-2011 |
nipkow <none@none> |
added simp lemma nth_Cons_pos to List
|
#
ab9a6cf0 |
|
03-Feb-2011 |
wenzelm <none@none> |
explicit is better than implicit;
|
#
36c8d8b8 |
|
11-Jan-2011 |
haftmann <none@none> |
"enriched_type" replaces less specific "type_lifting" --HG-- rename : src/HOL/Tools/type_lifting.ML => src/HOL/Tools/enriched_type.ML
|
#
8709b7e3 |
|
07-Jan-2011 |
bulwahn <none@none> |
adding simproc to rewrite list comprehensions to set comprehensions; adopting proofs
|
#
e8a2e703 |
|
21-Dec-2010 |
haftmann <none@none> |
tuned type_lifting declarations
|
#
adfe6cf9 |
|
17-Dec-2010 |
wenzelm <none@none> |
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
|
#
ce4d56f1 |
|
08-Dec-2010 |
haftmann <none@none> |
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
|
#
14dbdf06 |
|
06-Dec-2010 |
haftmann <none@none> |
replace `type_mapper` by the more adequate `type_lifting` --HG-- rename : src/HOL/Tools/type_mapper.ML => src/HOL/Tools/type_lifting.ML
|
#
9e4cf179 |
|
28-Nov-2010 |
nipkow <none@none> |
gave more standard finite set rules simp and intro attribute
|
#
2b6a6297 |
|
22-Nov-2010 |
bulwahn <none@none> |
adding code equations for EX1 on finite types
|
#
13e10bf0 |
|
18-Nov-2010 |
haftmann <none@none> |
mapper for list type; map_pair replaces prod_fun
|
#
9f6a4e58 |
|
17-Nov-2010 |
nipkow <none@none> |
code eqn for slice was missing; redefined splice with fun
|
#
270ce408 |
|
05-Nov-2010 |
bulwahn <none@none> |
added two lemmas about injectivity of concat to the list theory
|
#
9bdf4e57 |
|
02-Nov-2010 |
haftmann <none@none> |
lemmas sorted_map_same, sorted_same
|
#
5a1ada2b |
|
28-Oct-2010 |
nipkow <none@none> |
added lemmas about listrel(1)
|
#
b7ad03da |
|
27-Oct-2010 |
haftmann <none@none> |
sorting: avoid _key suffix if lemma applies both to simple and generalized variant; generalized insort_insert to insort_insert_key; additional lemmas
|
#
8c6f2b87 |
|
26-Oct-2010 |
haftmann <none@none> |
include ATP in theory List -- avoid theory edge by-passing the prominent list theory
|
#
0ff397f8 |
|
25-Oct-2010 |
haftmann <none@none> |
dropped (almost) redundant distinct.induct rule; distinct_simps again named distinct.simps
|
#
16a83284 |
|
24-Oct-2010 |
nipkow <none@none> |
nat_number -> eval_nat_numeral
|
#
37d247fe |
|
04-Oct-2010 |
blanchet <none@none> |
move Metis into Plain --HG-- rename : src/HOL/Tools/Sledgehammer/metis_reconstruct.ML => src/HOL/Tools/Metis/metis_reconstruct.ML rename : src/HOL/Tools/Sledgehammer/metis_tactics.ML => src/HOL/Tools/Metis/metis_tactics.ML rename : src/HOL/Tools/Sledgehammer/metis_translate.ML => src/HOL/Tools/Metis/metis_translate.ML
|
#
0f0b836a |
|
03-Oct-2010 |
haftmann <none@none> |
turned distinct and sorted into inductive predicates: yields nice induction principles for free; more elegant proofs
|
#
932ffb19 |
|
28-Sep-2010 |
haftmann <none@none> |
localized listsum
|
#
bc9ed6eb |
|
27-Sep-2010 |
haftmann <none@none> |
lemma remdups_map_remdups
|
#
a9cb65ea |
|
22-Sep-2010 |
nipkow <none@none> |
more lists lemmas
|
#
5b9e2150 |
|
20-Sep-2010 |
nipkow <none@none> |
new lemma
|
#
8aa90039 |
|
17-Sep-2010 |
haftmann <none@none> |
generalized lemma insort_remove1 to insort_key_remove1
|
#
5b59da77 |
|
13-Sep-2010 |
nipkow <none@none> |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
#
40bdb407 |
|
10-Sep-2010 |
haftmann <none@none> |
Haskell == is infix, not infixl
|
#
d96dfc41 |
|
26-Aug-2011 |
nipkow <none@none> |
added lemma
|
#
bb8268b1 |
|
07-Sep-2010 |
nipkow <none@none> |
expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
|
#
21414671 |
|
02-Sep-2010 |
hoelzl <none@none> |
Add filter_remove1
|
#
972f5d58 |
|
27-Aug-2010 |
haftmann <none@none> |
renamed class/constant eq to equal; tuned some instantiations
|
#
2ab2e08e |
|
25-Aug-2010 |
wenzelm <none@none> |
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
|
#
8c901cc8 |
|
19-Jul-2010 |
haftmann <none@none> |
Scala: subtle difference in printing strings vs. complex mixfix syntax
|
#
140c6b08 |
|
12-Jul-2010 |
haftmann <none@none> |
dropped superfluous [code del]s
|
#
7a5cf93d |
|
28-Jun-2010 |
haftmann <none@none> |
put section on distinctness before listsum; refined code generation operations; dropped ancient infix mem
|
#
69800ba8 |
|
18-Jun-2010 |
nipkow <none@none> |
tuned set_replicate lemmas
|
#
0bd17be8 |
|
18-Jun-2010 |
nipkow <none@none> |
added lemmas
|
#
e86a8293 |
|
18-Jun-2010 |
haftmann <none@none> |
made List.thy a join point in the theory graph
|
#
7054789d |
|
17-Jun-2010 |
haftmann <none@none> |
rev is reverse in Haskell
|
#
7e3c3490 |
|
13-Jun-2010 |
haftmann <none@none> |
use various predefined Haskell operations when generating code
|
#
b970a9f1 |
|
12-Jun-2010 |
haftmann <none@none> |
declare lexn.simps [code del]
|
#
cab686f5 |
|
02-Jun-2010 |
haftmann <none@none> |
induction over non-empty lists
|
#
907e6211 |
|
26-May-2010 |
haftmann <none@none> |
more convenient order of code equations
|
#
111ba9ae |
|
24-May-2010 |
haftmann <none@none> |
more lemmas
|
#
abaf09c1 |
|
20-May-2010 |
haftmann <none@none> |
turned old-style mem into an input abbreviation
|
#
b4935a1b |
|
14-May-2010 |
nipkow <none@none> |
added listsum lemmas
|
#
a6ca51b4 |
|
13-May-2010 |
nipkow <none@none> |
Multiset: renamed, added and tuned lemmas; Permutation: replaced local "remove" by List.remove1
|
#
41dbb802 |
|
12-May-2010 |
haftmann <none@none> |
added lemmas concerning last, butlast, insort
|
#
57b5e68a |
|
22-Apr-2010 |
haftmann <none@none> |
lemmas concerning remdups
|
#
a65fbeaf |
|
20-Apr-2010 |
hoelzl <none@none> |
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
|
#
bf999a3e |
|
18-Apr-2010 |
haftmann <none@none> |
more convenient equations for zip
|
#
82fe7ca2 |
|
16-Apr-2010 |
wenzelm <none@none> |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
#
f0c277f7 |
|
15-Apr-2010 |
Cezary Kaliszyk <kaliszyk@in.tum.de> |
Respectfullness and preservation of list_rel
|
#
206a5436 |
|
17-Mar-2010 |
blanchet <none@none> |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
#
eaf6f9f8 |
|
17-Mar-2010 |
blanchet <none@none> |
renamed "ATP_Linkup" theory to "Sledgehammer" --HG-- rename : src/HOL/ATP_Linkup.thy => src/HOL/Sledgehammer.thy
|
#
fd3ec919 |
|
06-Mar-2010 |
haftmann <none@none> |
added insort_insert
|
#
5ca1f212 |
|
05-Mar-2010 |
haftmann <none@none> |
moved lemma map_sorted_distinct_set_unique
|
#
c3541c58 |
|
02-Mar-2010 |
paulson <none@none> |
Slightly generalised a theorem
|
#
f8c1d1f1 |
|
21-Feb-2010 |
wenzelm <none@none> |
adapted to authentic syntax;
|
#
d34027db |
|
20-Feb-2010 |
haftmann <none@none> |
lemma distinct_insert
|
#
44f24eef |
|
20-Feb-2010 |
nipkow <none@none> |
added lemma
|
#
3aa9f578 |
|
19-Feb-2010 |
haftmann <none@none> |
moved remaning class operations from Algebras.thy to Groups.thy
|
#
aaaa7964 |
|
18-Feb-2010 |
huffman <none@none> |
get rid of many duplicate simp rule warnings
|
#
e31abfd7 |
|
18-Feb-2010 |
nipkow <none@none> |
added lemma
|
#
17d31541 |
|
17-Feb-2010 |
haftmann <none@none> |
more lemmas about sort(_key)
|
#
4f52a6da |
|
11-Feb-2010 |
wenzelm <none@none> |
modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;
|
#
5d17693c |
|
05-Feb-2010 |
haftmann <none@none> |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
#
85692e23 |
|
31-Jan-2010 |
haftmann <none@none> |
canonical insert operation; generalized lemma foldl_apply_inv to foldl_apply
|
#
d438ad75 |
|
19-Jan-2010 |
hoelzl <none@none> |
Added transpose_rectangle, when the input list is rectangular.
|
#
0cdd0727 |
|
19-Jan-2010 |
hoelzl <none@none> |
Add transpose to the List-theory.
|
#
74426e02 |
|
16-Jan-2010 |
haftmann <none@none> |
dropped some old primrecs and some constdefs
|
#
df118eed |
|
13-Jan-2010 |
haftmann <none@none> |
some syntax setup for Scala
|
#
870b91c3 |
|
10-Jan-2010 |
berghofe <none@none> |
same_append_eq / append_same_eq are now used for simplifying induction rules.
|
#
33d46a7f |
|
11-Dec-2009 |
haftmann <none@none> |
avoid dependency on implicit dest rule predicate1D in proofs
|
#
496367cb |
|
05-Dec-2009 |
haftmann <none@none> |
tuned lattices theory fragements; generlized some lemmas from sets to lattices
|
#
67adb92b |
|
04-Dec-2009 |
nipkow <none@none> |
added remdups_filter lemma
|
#
1a637a6c |
|
30-Nov-2009 |
haftmann <none@none> |
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML --HG-- rename : src/HOL/Tools/Datatype/datatype.ML => src/HOL/Tools/Datatype/datatype_data.ML extra : rebase_source : 552900fbf6783258465fa5000202d52cf1f99a1f
|
#
9f8ae5ab |
|
12-Nov-2009 |
hoelzl <none@none> |
Remove map_compose, replaced by map_map
|
#
207a2493 |
|
12-Nov-2009 |
hoelzl <none@none> |
New list theorems; added map_map to simpset, this is the prefered direction; allow sorting by a key
|
#
80b712c7 |
|
10-Nov-2009 |
haftmann <none@none> |
tuned imports
|
#
7d4dc9b8 |
|
29-Oct-2009 |
haftmann <none@none> |
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
|
#
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
|
#
f53404cd |
|
24-Sep-2009 |
haftmann <none@none> |
lemma relating fold1 and foldl; code_unfold rules for Inf_fin, Sup_fin, Min, Max, Inf, Sup
|
#
9b9a8ac4 |
|
27-Aug-2009 |
nipkow <none@none> |
code generator: quantifiers over {_.._::int} and {_..<_::nat} are now translated into (tail recursive) loops - no list is built.
|
#
dbb3d37a |
|
27-Aug-2009 |
nipkow <none@none> |
tuned code generation for lists
|
#
d018e244 |
|
26-Aug-2009 |
nipkow <none@none> |
got rid of complicated class finite_intvl_succ and defined "upto" directly on int, the only instance of the class.
|
#
a5a5665f |
|
15-Jul-2009 |
wenzelm <none@none> |
more antiquotations;
|
#
67d0648f |
|
15-Jul-2009 |
nipkow <none@none> |
Made "prime" executable
|
#
b932aaea |
|
14-Jul-2009 |
nipkow <none@none> |
made upt/upto executable on nat/int by simp
|
#
5c2bc460 |
|
14-Jul-2009 |
haftmann <none@none> |
prefer code_inline over code_unfold; use code_unfold_post where appropriate
|
#
fbe41aef |
|
14-Jul-2009 |
haftmann <none@none> |
code attributes use common underscore convention
|
#
04856658 |
|
03-Jul-2009 |
haftmann <none@none> |
lemma foldl_apply_inv
|
#
d0b33b8e |
|
23-Jun-2009 |
haftmann <none@none> |
tuned interfaces of datatype module
|
#
91b337ca |
|
19-Jun-2009 |
haftmann <none@none> |
discontinued ancient tradition to suffix certain ML module names with "_package" --HG-- rename : src/HOL/Import/import_package.ML => src/HOL/Import/import.ML rename : src/HOL/Nominal/nominal_package.ML => src/HOL/Nominal/nominal.ML rename : src/HOL/Tools/specification_package.ML => src/HOL/Tools/choice_specification.ML rename : src/HOL/Tools/datatype_package/datatype_package.ML => src/HOL/Tools/datatype_package/datatype.ML rename : src/HOL/Tools/function_package/fundef_package.ML => src/HOL/Tools/function_package/fundef.ML rename : src/HOL/Tools/inductive_package.ML => src/HOL/Tools/inductive.ML rename : src/HOL/Tools/inductive_set_package.ML => src/HOL/Tools/inductive_set.ML rename : src/HOL/Tools/old_primrec_package.ML => src/HOL/Tools/old_primrec.ML rename : src/HOL/Tools/primrec_package.ML => src/HOL/Tools/primrec.ML rename : src/HOL/Tools/recdef_package.ML => src/HOL/Tools/recdef.ML rename : src/HOL/Tools/record_package.ML => src/HOL/Tools/record.ML rename : src/HOL/Tools/typecopy_package.ML => src/HOL/Tools/typecopy.ML rename : src/HOL/Tools/typedef_package.ML => src/HOL/Tools/typedef.ML
|
#
7348f1d1 |
|
11-Jun-2009 |
nipkow <none@none> |
two finiteness lemmas by Robert Himmelmann
|
#
e76d0c51 |
|
04-Jun-2009 |
haftmann <none@none> |
lemma about List.foldl and Finite_Set.fold
|
#
b388003e |
|
02-Jun-2009 |
hoelzl <none@none> |
Added theorems about distinct & concat, map & replicate and concat & replicate
|
#
0d0ee217 |
|
26-May-2009 |
nipkow <none@none> |
more lemmas
|
#
f544c479 |
|
26-May-2009 |
huffman <none@none> |
listsum lemmas
|
#
4d32fa9f |
|
19-May-2009 |
nipkow <none@none> |
new lemma
|
#
e89997a7 |
|
15-May-2009 |
nipkow <none@none> |
new lemma
|
#
922dfe12 |
|
14-May-2009 |
haftmann <none@none> |
preprocessing must consider eq
|
#
6ca1bd25 |
|
08-May-2009 |
nipkow <none@none> |
lemmas by Andreas Lochbihler
|
#
188d7514 |
|
08-May-2009 |
nipkow <none@none> |
more lemmas
|
#
e1708bd6 |
|
06-May-2009 |
haftmann <none@none> |
proper structures for list and string code generation stuff
|
#
3b414c10 |
|
06-May-2009 |
haftmann <none@none> |
refined HOL string theories and corresponding ML fragments
|
#
64895fe4 |
|
29-Apr-2009 |
nipkow <none@none> |
added listsum lemmas
|
#
13866ee3 |
|
24-Apr-2009 |
haftmann <none@none> |
funpow and relpow with shared "^^" syntax
|
#
39f27693 |
|
20-Apr-2009 |
haftmann <none@none> |
power operation on functions with syntax o^; power operation on relations with syntax ^^
|
#
e743f6f0 |
|
17-Apr-2009 |
haftmann <none@none> |
separated funpow, relpow from power on monoids
|
#
121e82fb |
|
04-Mar-2009 |
blanchet <none@none> |
Merge.
|
#
bb2d682e |
|
02-Mar-2009 |
nipkow <none@none> |
name changes
|
#
2f2ef68c |
|
26-Feb-2009 |
huffman <none@none> |
revert some Suc 0 lemmas back to their original forms; added some simp rules for (1::nat)
|
#
77d6c0ba |
|
23-Feb-2009 |
huffman <none@none> |
make proofs work whether or not One_nat_def is a simp rule; replace 1 with Suc 0 in the rhs of some simp rules
|
#
bfd39a23 |
|
20-Feb-2009 |
haftmann <none@none> |
defensive implementation of pretty serialisation of lists and characters
|
#
459e8c8b |
|
16-Feb-2009 |
blanchet <none@none> |
Added nitpick attribute, and fixed typo.
|
#
7d2f2c1c |
|
10-Feb-2009 |
huffman <none@none> |
const_name antiquotations
|
#
1585463f |
|
07-Feb-2009 |
haftmann <none@none> |
code theorems for nth, list_update
|
#
1136dc43 |
|
07-Feb-2009 |
haftmann <none@none> |
code theorems for nth, list_update
|
#
2542e16d |
|
06-Feb-2009 |
haftmann <none@none> |
authentic syntax for List.nth
|
#
85f15bce |
|
03-Feb-2009 |
haftmann <none@none> |
dropped global Nil/Append interpretation
|
#
d6e70aa4 |
|
26-Jan-2009 |
haftmann <none@none> |
sorted_take, sorted_drop
|
#
7b4d17c7 |
|
16-Jan-2009 |
haftmann <none@none> |
migrated class package to new locale implementation
|
#
b15812f4 |
|
31-Dec-2008 |
wenzelm <none@none> |
eliminated OldTerm.add_term_free_names;
|
#
1be33ad4 |
|
31-Dec-2008 |
wenzelm <none@none> |
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
|
#
6d30ce6c |
|
11-Dec-2008 |
ballarin <none@none> |
Conversion of HOL-Main and ZF to new locales.
|
#
e01ddee4 |
|
04-Dec-2008 |
haftmann <none@none> |
cleaned up binding module and related code
|
#
39d5f60f |
|
17-Nov-2008 |
haftmann <none@none> |
tuned unfold_locales invocation
|
#
45f87f09 |
|
14-Nov-2008 |
haftmann <none@none> |
added length_unique operation for code generation
|
#
0842dc16 |
|
29-Oct-2008 |
haftmann <none@none> |
explicit check for pattern discipline before code translation
|
#
17442e49 |
|
22-Oct-2008 |
haftmann <none@none> |
code identifier namings are no longer imperative
|
#
85ca4f03 |
|
20-Oct-2008 |
nipkow <none@none> |
added lemmas
|
#
d63044b5 |
|
09-Oct-2008 |
haftmann <none@none> |
`code func` now just `code`
|
#
0a8ce6e7 |
|
09-Oct-2008 |
haftmann <none@none> |
established canonical argument order in SML code generators
|
#
c646a9a6 |
|
07-Oct-2008 |
haftmann <none@none> |
dropped superfluous if
|
#
6a52466d |
|
26-Sep-2008 |
haftmann <none@none> |
removed obsolete name convention "func"
|
#
1ea66695 |
|
25-Sep-2008 |
haftmann <none@none> |
discontinued special treatment of op = vs. eq_class.eq
|
#
5317e9bf |
|
17-Sep-2008 |
wenzelm <none@none> |
back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
|
#
8bdc29f0 |
|
16-Sep-2008 |
haftmann <none@none> |
a sophisticated char/nibble conversion combinator
|
#
d0e52819 |
|
16-Sep-2008 |
haftmann <none@none> |
explicit size of characters
|
#
8784a5be |
|
02-Sep-2008 |
haftmann <none@none> |
distributed literal code generation out of central infrastructure
|
#
63fad6d4 |
|
01-Sep-2008 |
nipkow <none@none> |
It appears that the code generator (Stefan's) needs some laws that appear superfluous: {..n} = set ...
|
#
fc8c2ee4 |
|
01-Sep-2008 |
nipkow <none@none> |
cleaned up code generation for {.._} and {..<_} moved lemmas into SetInterval where they belong
|
#
c2be4d61 |
|
01-Sep-2008 |
haftmann <none@none> |
restructured code generation of literals
|
#
7cbce2a5 |
|
28-Aug-2008 |
haftmann <none@none> |
restructured and split code serializer module
|
#
5b076103 |
|
31-Jul-2008 |
nipkow <none@none> |
made setsum executable on int.
|
#
4b2c0381 |
|
29-Jul-2008 |
nipkow <none@none> |
added removeAll
|
#
298265fc |
|
28-Jun-2008 |
wenzelm <none@none> |
@{lemma}: 'by' keyword;
|
#
ef956639 |
|
26-Jun-2008 |
haftmann <none@none> |
established Plain theory and image
|
#
8a6cac34 |
|
10-Jun-2008 |
haftmann <none@none> |
removed some dubious code lemmas
|
#
f0dd4ec0 |
|
23-May-2008 |
berghofe <none@none> |
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that set print_mode and margin appropriately.
|
#
37278cb8 |
|
12-May-2008 |
krauss <none@none> |
Measure functions can now be declared via special rules, allowing for a prolog-style generation of measure functions for a specific type.
|
#
a1ca9703 |
|
07-May-2008 |
berghofe <none@none> |
- Explicitely applied predicate1I in a few proofs, because it is no longer part of the claset - Explicitely passed pred_subset_eq and pred_equals_eq as an argument to the to_set attribute, because it is no longer applied automatically
|
#
d5ff3044 |
|
02-May-2008 |
nipkow <none@none> |
Added documentation
|
#
5dd85d40 |
|
25-Apr-2008 |
krauss <none@none> |
* New attribute "termination_simp": Simp rules for termination proofs * General lemmas about list_size
|
#
5a50fbc8 |
|
22-Apr-2008 |
haftmann <none@none> |
dropped some metis calls
|
#
c4165a78 |
|
08-Apr-2008 |
huffman <none@none> |
move lemmas from Word/BinBoolList.thy to List.thy
|
#
04e92685 |
|
29-Mar-2008 |
wenzelm <none@none> |
replaced 'ML_setup' by 'ML';
|
#
341cad20 |
|
27-Mar-2008 |
haftmann <none@none> |
restructuring; explicit case names for rule list_induct2
|
#
38095612 |
|
17-Mar-2008 |
wenzelm <none@none> |
removed duplicate lemmas;
|
#
9b283014 |
|
26-Feb-2008 |
haftmann <none@none> |
char and nibble are finite
|
#
4174e1a6 |
|
26-Feb-2008 |
bulwahn <none@none> |
Added useful general lemmas from the work with the HeapMonad
|
#
6f54a90c |
|
15-Feb-2008 |
nipkow <none@none> |
more lemmas
|
#
792ca356 |
|
25-Jan-2008 |
haftmann <none@none> |
dropped superfluous code theorems
|
#
778ab0d7 |
|
10-Jan-2008 |
berghofe <none@none> |
New interface for test data generators.
|
#
3e9f8d09 |
|
10-Dec-2007 |
haftmann <none@none> |
swtiched ATP_Linkup and PreList in theory hierarchy
|
#
c8abed18 |
|
07-Dec-2007 |
haftmann <none@none> |
instantiation target rather than legacy instance
|
#
b460ffd9 |
|
06-Dec-2007 |
haftmann <none@none> |
temporary code generator work arounds
|
#
3d4785e4 |
|
06-Dec-2007 |
haftmann <none@none> |
authentic primrec
|
#
732b4c9d |
|
29-Nov-2007 |
haftmann <none@none> |
instance command as rudimentary class target
|
#
beeb3cd4 |
|
05-Nov-2007 |
kleing <none@none> |
rev_nth
|
#
d95f4f2d |
|
05-Nov-2007 |
nipkow <none@none> |
added lemmas
|
#
762dfdcc |
|
05-Nov-2007 |
nipkow <none@none> |
added lemmas
|
#
3d7f5320 |
|
28-Oct-2007 |
wenzelm <none@none> |
append/member: more light-weight way to declare authentic syntax; tuned proofs;
|
#
091463a1 |
|
27-Oct-2007 |
krauss <none@none> |
use "fun" for definition of "member" -> authentic syntax
|
#
002c9527 |
|
23-Oct-2007 |
nipkow <none@none> |
went back to >0
|
#
1c05d4d6 |
|
23-Oct-2007 |
paulson <none@none> |
random tidying of proofs
|
#
3de058b3 |
|
21-Oct-2007 |
nipkow <none@none> |
Eliminated most of the neq0_conv occurrences. As a result, many theorems had to be rephrased with ~= 0 instead of > 0.
|
#
de474536 |
|
21-Oct-2007 |
wenzelm <none@none> |
avoid very slow metis invocation;
|
#
d8a0e4f0 |
|
19-Oct-2007 |
chaieb <none@none> |
fixed proofs
|
#
d9cf1af2 |
|
18-Oct-2007 |
haftmann <none@none> |
tuned
|
#
436aa0ff |
|
17-Oct-2007 |
nipkow <none@none> |
added sorted_list_of_set
|
#
d2ad869d |
|
16-Oct-2007 |
haftmann <none@none> |
global class syntax
|
#
6c5d0b14 |
|
08-Oct-2007 |
berghofe <none@none> |
list_codegen and char_codegen now call invoke_tycodegen to ensure that gen_... and term_of_... functions are generated as well.
|
#
b43776a1 |
|
01-Oct-2007 |
haftmann <none@none> |
added some lemmas
|
#
62ee215f |
|
29-Sep-2007 |
haftmann <none@none> |
proper syntax during class specification
|
#
6495a9ee |
|
24-Sep-2007 |
ballarin <none@none> |
Simplified proof due to improved integration of order_tac and simp.
|
#
93700273 |
|
25-Sep-2007 |
nipkow <none@none> |
hide successor
|
#
390db4b8 |
|
24-Sep-2007 |
nipkow <none@none> |
fixed haftmann bug
|
#
5820f3da |
|
20-Sep-2007 |
haftmann <none@none> |
fixed wrong syntax treatment in class target
|
#
5b1c4952 |
|
19-Sep-2007 |
nipkow <none@none> |
tuned
|
#
c5f12255 |
|
19-Sep-2007 |
paulson <none@none> |
metis too slow
|
#
67214e03 |
|
19-Sep-2007 |
nipkow <none@none> |
Generalized [_.._] from nat to linear orders
|
#
d547e2bb |
|
18-Sep-2007 |
ballarin <none@none> |
Simplified proofs due to transitivity reasoner setup.
|
#
bee08148 |
|
18-Sep-2007 |
paulson <none@none> |
metis now available in PreList
|
#
946bec84 |
|
17-Sep-2007 |
nipkow <none@none> |
sorting
|
#
a10709ef |
|
17-Sep-2007 |
nipkow <none@none> |
sorting
|
#
240f1bcf |
|
10-Sep-2007 |
nipkow <none@none> |
added lemma
|
#
42a6dcd8 |
|
04-Sep-2007 |
nipkow <none@none> |
tuned lemma; replaced !! by arbitrary
|
#
5bc22494 |
|
29-Aug-2007 |
nipkow <none@none> |
turned list comprehension translations into ML to optimize base case
|
#
68510184 |
|
29-Aug-2007 |
chaieb <none@none> |
removed unused theorems ; added lifting properties for foldr and foldl
|
#
313c0620 |
|
28-Aug-2007 |
berghofe <none@none> |
Changed "code" attribute of concat_map_singleton to "code unfold".
|
#
26dde658 |
|
28-Aug-2007 |
nipkow <none@none> |
added (code) lemmas for setsum and foldl
|
#
d72a89f7 |
|
20-Aug-2007 |
nipkow <none@none> |
Final mods for list comprehension
|
#
4e6cb65c |
|
20-Aug-2007 |
nipkow <none@none> |
removed allpairs - use list comprehension!
|
#
921871c0 |
|
17-Aug-2007 |
nipkow <none@none> |
removed set_concat_map and improved set_concat
|
#
35ae3509 |
|
14-Aug-2007 |
paulson <none@none> |
ATP blacklisting is now in theory data, attribute noatp
|
#
63a924b1 |
|
10-Aug-2007 |
haftmann <none@none> |
new structure for code generator modules
|
#
2dcc0991 |
|
07-Aug-2007 |
haftmann <none@none> |
new nbe implementation
|
#
595ac2e4 |
|
02-Aug-2007 |
berghofe <none@none> |
Repaired term_of_char.
|
#
b9b6c1b7 |
|
29-Jul-2007 |
wenzelm <none@none> |
proper simproc_setup for "list_neq";
|
#
00075772 |
|
25-Jul-2007 |
nipkow <none@none> |
Added lemmas
|
#
b584d2e2 |
|
24-Jul-2007 |
krauss <none@none> |
renamed lemma "set_take_whileD" to "set_takeWhileD"
|
#
a0eea0a9 |
|
11-Jul-2007 |
berghofe <none@none> |
Adapted to new package for inductive sets.
|
#
e1bd4929 |
|
03-Jul-2007 |
wenzelm <none@none> |
proper use of function_package ML files;
|
#
e53dff0a |
|
24-Jun-2007 |
nipkow <none@none> |
new lemmas
|
#
0c1bd92c |
|
14-Jun-2007 |
wenzelm <none@none> |
tuned proofs: avoid implicit prems; tuned partition proofs;
|
#
c0ce0021 |
|
06-Jun-2007 |
nipkow <none@none> |
tuned list comprehension, changed filter syntax from : to <-
|
#
7a3a7791 |
|
04-Jun-2007 |
chaieb <none@none> |
added a function partition and a few lemmas
|
#
de91d572 |
|
05-Jun-2007 |
chaieb <none@none> |
added a few theorems about foldl and set
|
#
d1e2a3d2 |
|
04-Jun-2007 |
nipkow <none@none> |
tuned list comprehension
|
#
bf1891ba |
|
04-Jun-2007 |
haftmann <none@none> |
authentic syntax for List.append
|
#
7c47f291 |
|
03-Jun-2007 |
wenzelm <none@none> |
renamed gen_submultiset to submultiset;
|
#
a526d15a |
|
03-Jun-2007 |
nipkow <none@none> |
tuned list comprehension, added lemma
|
#
29109c78 |
|
02-Jun-2007 |
nipkow <none@none> |
*** empty log message ***
|
#
50890dcd |
|
01-Jun-2007 |
nipkow <none@none> |
Moved list comprehension into List
|
#
83bee011 |
|
24-May-2007 |
nipkow <none@none> |
*** empty log message ***
|
#
542a44dc |
|
21-May-2007 |
haftmann <none@none> |
improved code for rev
|
#
b04c881c |
|
19-May-2007 |
haftmann <none@none> |
constant op @ now named append
|
#
531890cf |
|
17-May-2007 |
haftmann <none@none> |
abstract size function in hologic.ML
|
#
78c98741 |
|
11-May-2007 |
nipkow <none@none> |
*** empty log message ***
|
#
6ff08596 |
|
06-May-2007 |
haftmann <none@none> |
PreList imports RecDef
|
#
32a12bfb |
|
02-May-2007 |
nipkow <none@none> |
tuned allpairs
|
#
076c928a |
|
30-Apr-2007 |
nipkow <none@none> |
added allpairs
|
#
12a49000 |
|
26-Apr-2007 |
haftmann <none@none> |
moved code generation pretty integers and characters to separate theories
|
#
046fb1ff |
|
25-Apr-2007 |
nipkow <none@none> |
new lemma splice_length
|
#
46dd9685 |
|
11-Apr-2007 |
haftmann <none@none> |
tuned
|
#
38296483 |
|
30-Mar-2007 |
haftmann <none@none> |
paraphrasing equality
|
#
b014bad1 |
|
28-Mar-2007 |
berghofe <none@none> |
Improved code generator for characters: now handles non-printable characters as well.
|
#
1a56ea07 |
|
23-Mar-2007 |
haftmann <none@none> |
two further properties about lists
|
#
e2ef3abc |
|
21-Mar-2007 |
krauss <none@none> |
added another rule for simultaneous induction, and lemmas for zip
|
#
e1e12128 |
|
09-Mar-2007 |
haftmann <none@none> |
stepping towards uniform lattice theory development in HOL
|
#
1daf9028 |
|
07-Feb-2007 |
berghofe <none@none> |
Adapted to new inductive definition package.
|
#
eb237e6e |
|
21-Jan-2007 |
nipkow <none@none> |
Added simproc list_neq (prompted by an application)
|
#
afbb1e68 |
|
27-Dec-2006 |
haftmann <none@none> |
added OCaml code generation (without dictionaries)
|
#
4b4b36e9 |
|
21-Dec-2006 |
haftmann <none@none> |
added code lemmas for quantification over bounded nats
|
#
4e712509 |
|
18-Dec-2006 |
haftmann <none@none> |
added code generation syntax for some char combinators
|
#
d3648e5d |
|
13-Dec-2006 |
haftmann <none@none> |
clarified character setup
|
#
0272fffa |
|
10-Dec-2006 |
wenzelm <none@none> |
fixed term_of_list;
|
#
3eaac421 |
|
10-Dec-2006 |
wenzelm <none@none> |
moved char/string syntax to Tools/string_syntax.ML; HOLogic cleanup;
|
#
b24bc6be |
|
27-Nov-2006 |
haftmann <none@none> |
tuned keyword setup for SML code generator
|
#
f8f48251 |
|
22-Nov-2006 |
haftmann <none@none> |
incorporated structure HOList into HOLogic
|
#
cd65d9bc |
|
16-Nov-2006 |
wenzelm <none@none> |
more robust syntax for definition/abbreviation/notation;
|
#
ee3a2fff |
|
07-Nov-2006 |
krauss <none@none> |
Preparations for making "lexicographic_order" part of "fun"
|
#
00b42da0 |
|
06-Nov-2006 |
haftmann <none@none> |
removed itrev as inlining theorem
|
#
8d99bc11 |
|
01-Nov-2006 |
bulwahn <none@none> |
added lexicographic_order tactic
|
#
32a2fb05 |
|
31-Oct-2006 |
haftmann <none@none> |
adapted seralizer syntax
|
#
d4c61f5a |
|
31-Oct-2006 |
haftmann <none@none> |
adapted to new serializer syntax
|
#
62ee2095 |
|
26-Oct-2006 |
krauss <none@none> |
Added "recdef_wf" and "simp" attribute to "wf_measures"
|
#
0271bbab |
|
26-Oct-2006 |
krauss <none@none> |
Added "measures" combinator for lexicographic combinations of multiple measures.
|
#
1a2870c5 |
|
20-Oct-2006 |
haftmann <none@none> |
added reserved words for Haskell
|
#
0433ec71 |
|
20-Oct-2006 |
haftmann <none@none> |
added normal post setup; cleaned up "execution" constants
|
#
2002f725 |
|
16-Oct-2006 |
haftmann <none@none> |
moved HOL code generator setup to Code_Generator
|
#
0bae4103 |
|
25-Sep-2006 |
haftmann <none@none> |
refinements in codegen serializer
|
#
facb566c |
|
19-Sep-2006 |
haftmann <none@none> |
added operational equality
|
#
7517dca8 |
|
11-Sep-2006 |
wenzelm <none@none> |
induct method: renamed 'fixing' to 'arbitrary';
|
#
6117e276 |
|
01-Sep-2006 |
haftmann <none@none> |
final syntax for some Isar code generator keywords
|
#
a34bd496 |
|
30-Aug-2006 |
haftmann <none@none> |
code refinements
|
#
cb9a046f |
|
21-Aug-2006 |
haftmann <none@none> |
more concise string serialization
|
#
d8bb4109 |
|
14-Aug-2006 |
haftmann <none@none> |
simplified code generator setup
|
#
fab1b8c8 |
|
08-Aug-2006 |
haftmann <none@none> |
cleanup code generation for Numerals
|
#
745db1a3 |
|
26-Jul-2006 |
webertj <none@none> |
linear arithmetic splits certain operators (e.g. min, max, abs)
|
#
1bc5feec |
|
25-Jul-2006 |
haftmann <none@none> |
added code generator serialization for Char
|
#
92f6769a |
|
22-Jul-2006 |
haftmann <none@none> |
added structure HOList
|
#
bdc7891a |
|
21-Jul-2006 |
haftmann <none@none> |
added term_of_string function
|
#
7bbf8e26 |
|
12-Jul-2006 |
haftmann <none@none> |
adaptions in codegen
|
#
cfdc1311 |
|
07-Jul-2006 |
wenzelm <none@none> |
simprocs: no theory argument -- use simpset context instead;
|
#
2de288fd |
|
13-Jun-2006 |
haftmann <none@none> |
slight adaption for code generator
|
#
f4c6e262 |
|
07-Jun-2006 |
haftmann <none@none> |
slight code generator cleanup
|
#
cf24ee67 |
|
06-Jun-2006 |
haftmann <none@none> |
improved code lemmas
|
#
1a280064 |
|
05-Jun-2006 |
krauss <none@none> |
HOL/Tools/function_package: Added support for mutual recursive definitions.
|
#
d1dc012d |
|
12-May-2006 |
nipkow <none@none> |
added lemma in_measure
|
#
e7a4817a |
|
09-May-2006 |
haftmann <none@none> |
introduced characters for code generator; some improved code lemmas for some list functions
|
#
a61ca0d4 |
|
06-May-2006 |
wenzelm <none@none> |
removed 'concl is' patterns;
|
#
217ae5b3 |
|
27-Apr-2006 |
nipkow <none@none> |
added zip/take/drop lemmas
|
#
4f79d9cb |
|
09-Apr-2006 |
nipkow <none@none> |
Added function "splice"
|
#
b5d7d8ec |
|
08-Apr-2006 |
wenzelm <none@none> |
refined 'abbreviation';
|
#
2006d3ce |
|
20-Mar-2006 |
wenzelm <none@none> |
abbreviation upto, length;
|
#
0a5c5f88 |
|
25-Feb-2006 |
haftmann <none@none> |
improved codegen bootstrap
|
#
446dee87 |
|
23-Jan-2006 |
haftmann <none@none> |
removed problematic keyword 'atom'
|
#
75fddbe8 |
|
19-Jan-2006 |
wenzelm <none@none> |
setup: theory -> theory;
|
#
f662f0d2 |
|
18-Jan-2006 |
haftmann <none@none> |
substantial improvement in serialization handling
|
#
fe7871ca |
|
17-Jan-2006 |
haftmann <none@none> |
substantial improvements in code generator
|
#
27f3fea3 |
|
09-Jan-2006 |
paulson <none@none> |
theorems need names
|
#
d955c79b |
|
22-Dec-2005 |
nipkow <none@none> |
new lemmas
|
#
6ef4e683 |
|
21-Dec-2005 |
haftmann <none@none> |
slight clean ups
|
#
d9f4c279 |
|
20-Dec-2005 |
paulson <none@none> |
removed or modified some instances of [iff]
|
#
81f9ff25 |
|
16-Dec-2005 |
nipkow <none@none> |
new lemmas
|
#
9dcd7389 |
|
02-Dec-2005 |
krauss <none@none> |
Added recdef congruence rules for bounded quantifiers and commonly used higher order functions.
|
#
b39d2e23 |
|
30-Oct-2005 |
nipkow <none@none> |
A few new lemmas
|
#
8cceae71 |
|
21-Oct-2005 |
wenzelm <none@none> |
Goal.prove;
|
#
381fa8c3 |
|
18-Oct-2005 |
nipkow <none@none> |
added 2 lemmas
|
#
46e4168a |
|
17-Oct-2005 |
wenzelm <none@none> |
Simplifier.inherit_context instead of Simplifier.inherit_bounds;
|
#
9a82fe5a |
|
11-Oct-2005 |
nipkow <none@none> |
added hd lemma
|
#
cab20c91 |
|
05-Oct-2005 |
nipkow <none@none> |
added last in set lemma
|
#
39543642 |
|
04-Oct-2005 |
nipkow <none@none> |
new hd/rev/last lemmas
|
#
4925430d |
|
29-Sep-2005 |
paulson <none@none> |
simprules need names
|
#
c1b72c5f |
|
24-Sep-2005 |
nipkow <none@none> |
a few new filter lemmas
|
#
0789ab36 |
|
22-Sep-2005 |
nipkow <none@none> |
renamed rules to iprover
|
#
7d109468 |
|
20-Sep-2005 |
nipkow <none@none> |
added a number of lemmas
|
#
3e7cbaab |
|
17-Aug-2005 |
nipkow <none@none> |
small mods to code lemmas
|
#
8c6d1c49 |
|
16-Aug-2005 |
nipkow <none@none> |
added quite a few functions for code generation
|
#
8f769ddf |
|
02-Aug-2005 |
nipkow <none@none> |
Added filter lemma
|
#
678cd7d2 |
|
01-Aug-2005 |
wenzelm <none@none> |
simprocs: Simplifier.inherit_bounds;
|
#
74d535b0 |
|
01-Aug-2005 |
nipkow <none@none> |
added map_filter lemmas
|
#
c2997950 |
|
12-Jul-2005 |
berghofe <none@none> |
Auxiliary functions to be used in generated code are now defined using "attach".
|
#
0a703bd9 |
|
01-Jul-2005 |
berghofe <none@none> |
Adapted to new interface of code generator.
|
#
3f50877b |
|
15-Jun-2005 |
nipkow <none@none> |
added lemmas
|
#
c8f1dc34 |
|
27-Apr-2005 |
kleing <none@none> |
more on rev
|
#
93e610dd |
|
28-Apr-2005 |
kleing <none@none> |
more about list_update
|
#
c48de73e |
|
10-Apr-2005 |
nipkow <none@none> |
tuned Map, renamed lex stuff in List.
|
#
7c495aa9 |
|
05-Apr-2005 |
paulson <none@none> |
lexicographic order by Norbert Voelker
|
#
eee46a1e |
|
02-Mar-2005 |
skalberg <none@none> |
Move towards standard functions.
|
#
3dffd254 |
|
13-Feb-2005 |
skalberg <none@none> |
Deleted Library.option type.
|
#
608be601 |
|
02-Feb-2005 |
berghofe <none@none> |
Replaced application of subst by simplesubst in proof of rev_induct to avoid problems with program extraction.
|
#
657298fd |
|
13-Jan-2005 |
nipkow <none@none> |
made diff_less a simp rule
|
#
e669f42f |
|
03-Jan-2005 |
kleing <none@none> |
added list_all_rev
|
#
d2f26441 |
|
22-Dec-2004 |
nipkow <none@none> |
[ .. (] -> [ ..< ]
|
#
4fe6092b |
|
09-Dec-2004 |
nipkow <none@none> |
First step in reorganizing Finite_Set
|
#
387d9caa |
|
22-Nov-2004 |
paulson <none@none> |
indentation
|
#
2b77596b |
|
22-Nov-2004 |
nipkow <none@none> |
added lemmas
|
#
82c20b4c |
|
21-Nov-2004 |
nipkow <none@none> |
Added more lemmas
|
#
3f348152 |
|
21-Nov-2004 |
nipkow <none@none> |
added lemmas
|
#
71f87ec4 |
|
20-Nov-2004 |
nipkow <none@none> |
Restructured List and added "rotate"
|
#
51932445 |
|
12-Nov-2004 |
nipkow <none@none> |
More lemmas
|
#
997b6b04 |
|
19-Oct-2004 |
paulson <none@none> |
converted some induct_tac to induct
|
#
d71e3359 |
|
15-Oct-2004 |
nipkow <none@none> |
added and renamed
|
#
53b8dc83 |
|
13-Oct-2004 |
nipkow <none@none> |
Added a few lemmas
|
#
34bbf13d |
|
10-Oct-2004 |
nipkow <none@none> |
Proofs needed to be updated because induction now preserves name of induction variable.
|
#
c1529bde |
|
03-Sep-2004 |
paulson <none@none> |
listrel operator for lifting relations to lists
|
#
09eb9abb |
|
01-Sep-2004 |
paulson <none@none> |
new functions for sets of lists
|
#
0fe1d442 |
|
18-Aug-2004 |
nipkow <none@none> |
import -> imports
|
#
e61c8d7d |
|
16-Aug-2004 |
nipkow <none@none> |
New theory header syntax.
|
#
169c5045 |
|
05-Aug-2004 |
paulson <none@none> |
some structured proofs
|
#
22382750 |
|
04-Aug-2004 |
nipkow <none@none> |
Added a number of new thms and the new function remove1
|
#
451f9035 |
|
22-Jul-2004 |
paulson <none@none> |
new material courtesy of Norbert Voelker
|
#
3bdc4d6c |
|
19-Jul-2004 |
berghofe <none@none> |
- Moved code generator setup for lists from Main.thy to List.thy - Code generator now represents char type as strings of length 1 (easier to handle than encoding using nibbles)
|
#
2a98d8d4 |
|
15-Jul-2004 |
nipkow <none@none> |
Moved to new m<..<n syntax for set intervals.
|
#
33b1b845 |
|
21-Jun-2004 |
kleing <none@none> |
Merged in license change from Isabelle2004
|
#
7c8e76a3 |
|
24-May-2004 |
nipkow <none@none> |
added drop_take:thm
|
#
9e0da269 |
|
21-May-2004 |
wenzelm <none@none> |
removed duplicate thms;
|
#
f499cf68 |
|
16-Apr-2004 |
mehta <none@none> |
lemma drop_Suc_conv_tl added.
|
#
c9ad039a |
|
16-Apr-2004 |
wenzelm <none@none> |
tuned document;
|
#
cd257618 |
|
14-Apr-2004 |
kleing <none@none> |
use more symbols in HTML output
|
#
38bb91bf |
|
12-Apr-2004 |
oheimb <none@none> |
removed o2l and fold_rel; moved postfix to Library/List_Prefix.thy
|
#
e77abee1 |
|
29-Mar-2004 |
nipkow <none@none> |
Added append_eq_append_conv2
|
#
5c9ec06d |
|
19-Feb-2004 |
nipkow <none@none> |
moved lemmas from MicroJava/Comp/AuxLemmas.thy to List.thy
|
#
f8a0b9d7 |
|
19-Feb-2004 |
paulson <none@none> |
new theorem
|
#
41bcec42 |
|
15-Feb-2004 |
kleing <none@none> |
lemmas about card (set xs)
|
#
7e679f7b |
|
06-Jan-2004 |
kleing <none@none> |
map_idI
|
#
64559537 |
|
05-Jan-2004 |
nipkow <none@none> |
*** empty log message ***
|
#
aac3cbde |
|
05-Jan-2004 |
nipkow <none@none> |
*** empty log message ***
|
#
989b2cdb |
|
24-Dec-2003 |
kleing <none@none> |
list_all2_nthD no good as [intro?]
|
#
2dd43ad3 |
|
23-Dec-2003 |
kleing <none@none> |
list_all2_mono should not be [trans]
|
#
b1de4c3e |
|
22-Dec-2003 |
kleing <none@none> |
added some [intro?] and [trans] for list_all2 lemmas
|
#
51fbac88 |
|
18-Dec-2003 |
nipkow <none@none> |
*** empty log message ***
|
#
36f64ffe |
|
18-Dec-2003 |
nipkow <none@none> |
*** empty log message ***
|
#
3c5d5d27 |
|
28-Oct-2003 |
nipkow <none@none> |
*** empty log message ***
|
#
b79b3996 |
|
26-Sep-2003 |
paulson <none@none> |
misc tidying
|
#
86601865 |
|
14-Sep-2003 |
nipkow <none@none> |
Added new theorems
|
#
ecabeee0 |
|
15-Jul-2003 |
nipkow <none@none> |
Some new thm (ex_map_conv?)
|
#
55c45f1f |
|
11-Jul-2003 |
oheimb <none@none> |
added fold_red, o2l, postfix, some thms
|
#
5b181ce5 |
|
28-May-2003 |
paulson <none@none> |
new theorem
|
#
efd5dc29 |
|
14-May-2003 |
nipkow <none@none> |
*** empty log message ***
|
#
315c6710 |
|
16-Apr-2003 |
nipkow <none@none> |
Added take/dropWhile thms
|
#
030fb954 |
|
25-Mar-2003 |
berghofe <none@none> |
Re-structured some proofs in order to get rid of rule_format attribute.
|
#
1dac116a |
|
13-Mar-2003 |
kleing <none@none> |
more about list_all2
|
#
9255c907 |
|
29-Nov-2002 |
nipkow <none@none> |
added a few lemmas
|
#
74d67fdb |
|
30-Sep-2002 |
berghofe <none@none> |
Adapted to new simplifier.
|
#
4803de87 |
|
26-Sep-2002 |
paulson <none@none> |
Converted Fun to Isar style. Moved Pi, funcset, restrict from Fun.thy to Library/FuncSet.thy. Renamed constant "Fun.op o" to "Fun.comp"
|
#
4d97d0af |
|
21-Aug-2002 |
paulson <none@none> |
Frederic Blanqui's new "guard" examples
|
#
0553df8d |
|
08-Aug-2002 |
wenzelm <none@none> |
use Tactic.prove instead of prove_goalw_cterm in internal proofs!
|
#
1f05977e |
|
06-Aug-2002 |
wenzelm <none@none> |
sane interface for simprocs;
|
#
d4a94812 |
|
16-Jul-2002 |
wenzelm <none@none> |
moved stuff from Main.thy; tuned;
|
#
3690eeb2 |
|
30-May-2002 |
nipkow <none@none> |
Modifications due to enhanced linear arithmetic.
|
#
45fe95fd |
|
13-May-2002 |
nipkow <none@none> |
*** empty log message ***
|
#
4b457942 |
|
13-May-2002 |
nipkow <none@none> |
*** empty log message ***
|
#
a0639b13 |
|
13-May-2002 |
nipkow <none@none> |
*** empty log message ***
|
#
e56c6e04 |
|
13-May-2002 |
wenzelm <none@none> |
tuned document;
|
#
93f64880 |
|
08-May-2002 |
nipkow <none@none> |
new thm distinct_conv_nth
|
#
a8d350b4 |
|
07-May-2002 |
wenzelm <none@none> |
oops;
|
#
22476bb4 |
|
07-May-2002 |
wenzelm <none@none> |
converted;
|
#
b3655ff2 |
|
14-Feb-2002 |
nipkow <none@none> |
nodups -> distinct
|
#
c1694cb4 |
|
08-Nov-2001 |
wenzelm <none@none> |
eliminated old "symbols" syntax, use "xsymbols" instead;
|
#
ee7fa931 |
|
09-Jan-2001 |
nipkow <none@none> |
`` -> and ``` -> ``
|
#
98ca4e12 |
|
16-Jul-2000 |
wenzelm <none@none> |
avoid 'split';
|
#
9c19b0f1 |
|
14-Jul-2000 |
oheimb <none@none> |
tuned syntax
|
#
4d399edf |
|
14-Jul-2000 |
paulson <none@none> |
moved sublist from UNITY/AllocBase to List
|
#
18c1f4c7 |
|
26-May-2000 |
paulson <none@none> |
named the primrec clauses of upt
|
#
a95b3c39 |
|
25-May-2000 |
paulson <none@none> |
better indentation; declared function "null"
|
#
006bc991 |
|
15-May-2000 |
berghofe <none@none> |
Removed unnecessary primrec equations of hd and last involving arbitrary.
|
#
dc3bc48c |
|
13-Apr-2000 |
nipkow <none@none> |
Times -> <*> ** -> <*lex*>
|
#
17698718 |
|
15-Mar-2000 |
wenzelm <none@none> |
added HOL/PreLIst.thy;
|
#
4aeea2f4 |
|
10-Jan-2000 |
nipkow <none@none> |
Forgot to "call" MicroJava in makefile. Added list_all2 to List.
|
#
aefedbe0 |
|
04-Nov-1999 |
paulson <none@none> |
added foldr
|
#
888d07b6 |
|
16-Aug-1999 |
wenzelm <none@none> |
'a list: Nil, Cons;
|
#
ba8b30c8 |
|
19-Jul-1999 |
paulson <none@none> |
NatBin: binary arithmetic for the naturals
|
#
d8b4d871 |
|
01-Apr-1999 |
pusch <none@none> |
new definition for nth. added warnings, if primrec definition is deleted from simpset.
|
#
2254386e |
|
08-Mar-1999 |
nipkow <none@none> |
modified zip
|
#
47c871ae |
|
19-Jan-1999 |
paulson <none@none> |
removal of the (thm list) argument of mk_cases
|
#
831fd1e4 |
|
21-Sep-1998 |
oheimb <none@none> |
re-added mem and list_all
|
#
06ef1e97 |
|
09-Sep-1998 |
oheimb <none@none> |
changed constants mem and list_all to mere translations added filter_is_subset
|
#
e4589f38 |
|
04-Sep-1998 |
nipkow <none@none> |
Arith: less_diff_conv List: [i..j]
|
#
d4256399 |
|
02-Sep-1998 |
nipkow <none@none> |
Added function upto to List. Had to rearrange loading sequence because now List uses Recdef.
|
#
33b89906 |
|
12-Aug-1998 |
oheimb <none@none> |
replaced idt by pttrn in @filter
|
#
bac1f823 |
|
08-Aug-1998 |
nipkow <none@none> |
List now contains some lexicographic orderings.
|
#
df41c559 |
|
24-Jul-1998 |
berghofe <none@none> |
Adapted to new datatype package.
|
#
10774599 |
|
20-Jul-1998 |
nipkow <none@none> |
Added simproc list_eq.
|
#
0dca510d |
|
24-Jun-1998 |
nipkow <none@none> |
* 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,...].
|
#
da4ba212 |
|
22-Feb-1998 |
nipkow <none@none> |
New induction schemas for lists (length and snoc).
|
#
86a060a2 |
|
06-Feb-1998 |
nipkow <none@none> |
Added `remdups' nodup -> nodups
|
#
ff315cf5 |
|
30-Dec-1997 |
nipkow <none@none> |
nth -> !
|
#
25504a5b |
|
05-Nov-1997 |
wenzelm <none@none> |
adapted typed_print_translation;
|
#
220d8bda |
|
04-Nov-1997 |
oheimb <none@none> |
added zip and nodup
|
#
173331d8 |
|
16-Oct-1997 |
nipkow <none@none> |
Various new lemmas. Improved conversion of equations to rewrite rules: (s=t becomes (s=t)==True if s=t loops).
|
#
39c87116 |
|
10-Oct-1997 |
wenzelm <none@none> |
fixed dots;
|
#
5ba3363d |
|
05-Aug-1997 |
nipkow <none@none> |
Added function `replicate' and lemmas map_cong and set_replicate.
|
#
f463cc59 |
|
01-Aug-1997 |
nipkow <none@none> |
Corected bug in def of dropWhile (also present in Haskell lib!)
|
#
23dc3d64 |
|
08-Jul-1997 |
nipkow <none@none> |
Improved length = size translation.
|
#
8628ff0b |
|
26-Jun-1997 |
nipkow <none@none> |
set_of_list -> set
|
#
a005c862 |
|
16-Jun-1997 |
paulson <none@none> |
Replacing the primrec definition of "length" by a translation to the built-in "size" function
|
#
73efee82 |
|
05-Jun-1997 |
paulson <none@none> |
Deleted the obsolete "pred_list" relation
|
#
92f947e8 |
|
30-May-1997 |
paulson <none@none> |
Now Divides must be the parent
|
#
5ab8e8f7 |
|
25-May-1997 |
paulson <none@none> |
New operator "lists" for formalizing sets of lists
|
#
fefe191e |
|
23-May-1997 |
nipkow <none@none> |
Added `arbitrary'
|
#
ce904e8a |
|
14-May-1997 |
paulson <none@none> |
Added pred_list for TFL
|
#
0af5293c |
|
06-Mar-1997 |
pusch <none@none> |
primrec definition for nth
|
#
da1498de |
|
12-Feb-1997 |
nipkow <none@none> |
New class "order" and accompanying changes. In particular reflexivity of <= is now one rewrite rule.
|
#
55eee2cf |
|
17-Jan-1997 |
nipkow <none@none> |
Got rid of Alls in List. Added Ball_insert and Ball_Un in equalities.ML.
|
#
994ff94d |
|
10-Dec-1996 |
wenzelm <none@none> |
removed ambiguous symbols syntax;
|
#
59d8eb4d |
|
27-Nov-1996 |
wenzelm <none@none> |
added symbols syntax;
|
#
7f54436f |
|
19-Aug-1996 |
paulson <none@none> |
Renamed setOfList to set_of_list
|
#
66a43fca |
|
01-Aug-1996 |
berghofe <none@none> |
Simplified primrec definitions.
|
#
3e181545 |
|
25-Jun-1996 |
berghofe <none@none> |
Changed argument order of nat_rec.
|
#
bb54651a |
|
18-Jun-1996 |
paulson <none@none> |
Addition of setOfList
|
#
1d43e2fa |
|
05-Feb-1996 |
clasohm <none@none> |
expanded tabs; renamed subtype to typedef; incorporated Konrad's changes
|
#
35cd766f |
|
21-Dec-1995 |
nipkow <none@none> |
defined take/drop by induction over list rather than nat.
|
#
53d84dbd |
|
29-Nov-1995 |
clasohm <none@none> |
removed quotes from types in consts and syntax sections
|
#
3b7267a2 |
|
12-Nov-1995 |
nipkow <none@none> |
added new arithmetic lemmas and the functions take and drop.
|
#
9fff7d2f |
|
29-Jun-1995 |
lcp <none@none> |
Added function rev and its properties length_rev, etc.
|
#
2c493bbc |
|
27-Mar-1995 |
clasohm <none@none> |
changed syntax of datatype declarations (curried types for constructor parameters)
|
#
e179ae2e |
|
20-Mar-1995 |
clasohm <none@none> |
changed syntax of "if"
|
#
46f10ec6 |
|
02-Mar-1995 |
clasohm <none@none> |
new version of HOL with curried function application
|