#
0635ff6c |
|
25-Feb-2020 |
paulson <lp15@cam.ac.uk> |
Moved a number of general-purpose lemmas into HOL
|
#
3748b095 |
|
23-Feb-2020 |
paulson <lp15@cam.ac.uk> |
a few new lemmas
|
#
0c4f403a |
|
27-Jan-2020 |
paulson <lp15@cam.ac.uk> |
A few lemmas connected with orderings
|
#
6ce8882b |
|
14-Mar-2019 |
wenzelm <none@none> |
more specific keyword kinds;
|
#
e977f1fa |
|
31-Jan-2019 |
haftmann <none@none> |
proper congruence rule for image operator --HG-- extra : rebase_source : 71f59936260619419f4d3f7f86d1b930bc771065
|
#
ffdb775d |
|
24-Jan-2019 |
paulson <lp15@cam.ac.uk> |
the theory of Equipollence, and moving Fpow from Cardinals into Main
|
#
083015db |
|
21-Jan-2019 |
paulson <lp15@cam.ac.uk> |
new material about summations and powers, along with some tweaks
|
#
504acaca |
|
14-Jan-2019 |
haftmann <none@none> |
tuned proofs
|
#
e60cf64d |
|
06-Jan-2019 |
wenzelm <none@none> |
isabelle update -u path_cartouches;
|
#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
05936fb0 |
|
23-Dec-2018 |
haftmann <none@none> |
more rules
|
#
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
#
1387b04b |
|
19-Dec-2017 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
30dac60d |
|
10-Mar-2017 |
haftmann <none@none> |
restored surj as output abbreviation, amending 6af79184bef3
|
#
229f8947 |
|
29-Jan-2017 |
wenzelm <none@none> |
added inj_def (redundant, analogous to surj_def, bij_def); tuned proofs;
|
#
ddc7c7d3 |
|
29-Jan-2017 |
wenzelm <none@none> |
tuned proofs;
|
#
4693ea2d |
|
02-Aug-2016 |
wenzelm <none@none> |
tuned proof;
|
#
f937778a |
|
02-Aug-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
#
8806de60 |
|
01-Aug-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
#
65b76842 |
|
29-Jul-2016 |
Andreas Lochbihler <none@none> |
add lemmas contributed by Peter Gammie
|
#
d16ece07 |
|
08-Jul-2016 |
haftmann <none@none> |
avoid to hide equality behind (output) abbreviation
|
#
b78a0c93 |
|
05-Jul-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
#
0f0a91d1 |
|
02-Jul-2016 |
haftmann <none@none> |
more theorems
|
#
84979e2b |
|
20-Jun-2016 |
wenzelm <none@none> |
prefer HOL definitions;
|
#
bf8332e3 |
|
20-Jun-2016 |
wenzelm <none@none> |
tuned proof;
|
#
eab922d6 |
|
20-Jun-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
#
6396ec02 |
|
09-May-2016 |
paulson <lp15@cam.ac.uk> |
renamings and refinements
|
#
0700f7dc |
|
04-Apr-2016 |
paulson <lp15@cam.ac.uk> |
Mostly renaming (from HOL Light to Isabelle conventions), with a couple of new results
|
#
60a0b6b0 |
|
14-Mar-2016 |
paulson <lp15@cam.ac.uk> |
Refactoring (moving theorems into better locations), plus a bit of new material
|
#
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
#
0bfb73b6 |
|
28-Dec-2015 |
wenzelm <none@none> |
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
|
#
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
|
#
3487f527 |
|
11-Nov-2015 |
Andreas Lochbihler <none@none> |
add various lemmas
|
#
6daef852 |
|
27-Oct-2015 |
paulson <lp15@cam.ac.uk> |
Cauchy's integral formula, required lemmas, and a bit of reorganisation
|
#
607ae3e3 |
|
09-Oct-2015 |
wenzelm <none@none> |
discontinued specific HTML syntax;
|
#
33d48711 |
|
21-Sep-2015 |
paulson <none@none> |
new lemmas and movement of lemmas into place
|
#
4e357ed3 |
|
13-Aug-2015 |
haftmann <none@none> |
more lemmas --HG-- extra : rebase_source : 629d5d21c15fc4a23007104e9f5a8ccccbad1886
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
eb3596fa |
|
26-May-2015 |
paulson <none@none> |
New material about paths, and some lemmas
|
#
c88911fe |
|
11-Feb-2015 |
Andreas Lochbihler <none@none> |
add lemmas about bind and image
|
#
7145f505 |
|
10-Feb-2015 |
paulson <lp15@cam.ac.uk> |
New lemmas and a bit of tidying up.
|
#
b8d56fe6 |
|
10-Feb-2015 |
wenzelm <none@none> |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
233ef912 |
|
30-Oct-2014 |
wenzelm <none@none> |
eliminated aliases;
|
#
caa51abc |
|
06-Sep-2014 |
haftmann <none@none> |
added various facts
|
#
fecf4a1c |
|
01-Sep-2014 |
blanchet <none@none> |
tuned structure inclusion
|
#
c67db02e |
|
21-Jun-2014 |
ballarin <none@none> |
Two basic lemmas on bij_betw.
|
#
edaea794 |
|
16-Apr-2014 |
haftmann <none@none> |
more simp rules for Fun.swap
|
#
88cc155c |
|
15-Mar-2014 |
haftmann <none@none> |
more complete set of lemmas wrt. image and composition
|
#
462f1580 |
|
13-Mar-2014 |
haftmann <none@none> |
tuned proofs
|
#
42fc4ea5 |
|
09-Mar-2014 |
haftmann <none@none> |
bootstrap fundamental Fun theory immediately after Set theory, without dependency on complete lattices * * * tuned
|
#
da328fb3 |
|
07-Mar-2014 |
wenzelm <none@none> |
more antiquotations;
|
#
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
|
#
63970edd |
|
12-Feb-2014 |
blanchet <none@none> |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
#
9e021ec0 |
|
20-Jan-2014 |
blanchet <none@none> |
tuning
|
#
e61ebd88 |
|
16-Jan-2014 |
blanchet <none@none> |
moved lemmas from 'Fun_More_FP' to where they belong
|
#
b7a6808f |
|
25-Nov-2013 |
traytel <none@none> |
eliminated dependence of BNF on Infinite_Set by moving 3 theorems from the latter to Main
|
#
03633065 |
|
18-Oct-2013 |
blanchet <none@none> |
killed most "no_atp", to make Sledgehammer more complete
|
#
8c550eac |
|
26-Sep-2013 |
Andreas Lochbihler <none@none> |
add lemmas
|
#
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
|
#
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
#
cef4a7ce |
|
03-Apr-2013 |
haftmann <none@none> |
generalized lemma fold_image thanks to Peter Lammich
|
#
c1d9f321 |
|
18-Oct-2012 |
haftmann <none@none> |
simp results for simplification results of Inf/Sup expressions on bool; tuned proofs
|
#
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;
|
#
e13bdbb0 |
|
19-Apr-2012 |
huffman <none@none> |
tuned lemmas (v)image_id; removed duplicate of vimage_id --HG-- extra : rebase_source : 9178db2e0f900cdeab723f13b8c0d5fc45786a95
|
#
f928efd2 |
|
15-Apr-2012 |
haftmann <none@none> |
centralized enriched_type declaration, thanks to in-situ available Isar commands --HG-- extra : rebase_source : ea8947ffa8bb301d674c472c3427994b31c4c458
|
#
870593bf |
|
15-Mar-2012 |
wenzelm <none@none> |
declare command keywords via theory header, including strict checking outside Pure;
|
#
bb514778 |
|
22-Feb-2012 |
bulwahn <none@none> |
generalizing inj_on_Int
|
#
0505fb5e |
|
05-Feb-2012 |
bulwahn <none@none> |
removing lemma bij_betw_Disj_Un, as it is a special case of bij_between_combine (was added in d1fc454d6735, and has not been used since)
|
#
e9fa6982 |
|
05-Feb-2012 |
bulwahn <none@none> |
adding a remark about lemma which is too special and should be removed
|
#
9c29febc |
|
20-Nov-2011 |
wenzelm <none@none> |
explicit is better than implicit;
|
#
0042ace4 |
|
19-Oct-2011 |
bulwahn <none@none> |
removing old code generator setup for function types
|
#
15635718 |
|
13-Sep-2011 |
huffman <none@none> |
tuned proofs
|
#
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
|
#
d04d4aee |
|
10-Sep-2011 |
haftmann <none@none> |
renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc. --HG-- rename : src/HOL/Complete_Lattice.thy => src/HOL/Complete_Lattices.thy
|
#
4c98af0b |
|
06-Sep-2011 |
nipkow <none@none> |
added new lemmas
|
#
9f9757b8 |
|
18-Aug-2011 |
haftmann <none@none> |
moved fundamental lemma fun_eq_iff to theory HOL; tuned whitespace
|
#
b50b6583 |
|
27-Jul-2011 |
hoelzl <none@none> |
finite vimage on arbitrary domains
|
#
9da02764 |
|
17-Jul-2011 |
haftmann <none@none> |
more on complement
|
#
efb08dc8 |
|
07-Jul-2011 |
nipkow <none@none> |
added translation to fix critical pair between abbreviations for surj and ~=
|
#
c47b7e16 |
|
20-May-2011 |
hoelzl <none@none> |
add surj_vimage_empty
|
#
78aea85a |
|
05-Apr-2011 |
blanchet <none@none> |
added "no_atp" to Cantor's paradox
|
#
5ab5866e |
|
21-Jan-2011 |
haftmann <none@none> |
moved theorem
|
#
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
|
#
adfe6cf9 |
|
17-Dec-2010 |
wenzelm <none@none> |
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
|
#
2049fb8d |
|
06-Dec-2010 |
haftmann <none@none> |
moved bootstrap of type_lifting to Fun
|
#
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
|
#
452856fc |
|
26-Nov-2010 |
wenzelm <none@none> |
keep private things private, without comments;
|
#
b1068d3f |
|
23-Nov-2010 |
hoelzl <none@none> |
Move some missing lemmas from Andrei Popescus 'Ordinals and Cardinals' AFP entry to the HOL-image.
|
#
b97be2fb |
|
22-Nov-2010 |
hoelzl <none@none> |
Replace surj by abbreviation; remove surj_on.
|
#
172e431c |
|
18-Nov-2010 |
haftmann <none@none> |
map_fun combinator in theory Fun
|
#
5b59da77 |
|
13-Sep-2010 |
nipkow <none@none> |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
#
35d51202 |
|
08-Sep-2010 |
nipkow <none@none> |
put expand_(fun/set)_eq back in as synonyms, for compatibility
|
#
bb8268b1 |
|
07-Sep-2010 |
nipkow <none@none> |
expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
|
#
96d9b912 |
|
02-Sep-2010 |
hoelzl <none@none> |
Revert bij_betw changes to simp set (Problem in afp/Ordinals_and_Cardinals)
|
#
401d8afc |
|
02-Sep-2010 |
hoelzl <none@none> |
Introduce surj_on and replace surj and bij by abbreviations.
|
#
7f4af77a |
|
02-Sep-2010 |
hoelzl <none@none> |
Permutation implies bij function
|
#
fee3b98b |
|
02-Sep-2010 |
hoelzl <none@none> |
bij <--> bij_betw
|
#
b244bd5e |
|
20-Aug-2010 |
haftmann <none@none> |
inj_comp and inj_fun
|
#
140c6b08 |
|
12-Jul-2010 |
haftmann <none@none> |
dropped superfluous [code del]s
|
#
8c105c87 |
|
09-Jul-2010 |
haftmann <none@none> |
nicer xsymbol syntax for fcomp and scomp
|
#
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;
|
#
14a1c633 |
|
05-Mar-2010 |
hoelzl <none@none> |
generalized inj_uminus; added strict_mono_imp_inj_on
|
#
aef92ff7 |
|
04-Mar-2010 |
hoelzl <none@none> |
Rewrite rules for images of minus of intervals
|
#
baea5702 |
|
01-Mar-2010 |
haftmann <none@none> |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
#
4f52a6da |
|
11-Feb-2010 |
wenzelm <none@none> |
modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;
|
#
6cb03d83 |
|
30-Dec-2009 |
krauss <none@none> |
killed a few warnings
|
#
e0f4f608 |
|
21-Dec-2009 |
haftmann <none@none> |
moved lemmas o_eq_dest, o_eq_elim here
|
#
83275e13 |
|
18-Dec-2009 |
huffman <none@none> |
add lemma swap_triple
|
#
17a76c81 |
|
16-Dec-2009 |
huffman <none@none> |
declare swap_self [simp], add lemma comp_swap
|
#
7d4dc9b8 |
|
29-Oct-2009 |
haftmann <none@none> |
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
|
#
179dc521 |
|
22-Oct-2009 |
nipkow <none@none> |
inv_onto -> inv_into
|
#
ee2c102c |
|
20-Oct-2009 |
paulson <none@none> |
Some new lemmas concerning sets
|
#
4806d9ad |
|
19-Oct-2009 |
berghofe <none@none> |
Renamed inv to the_inv and turned it into an abbreviation (based on the_inv_onto).
|
#
def242e4 |
|
17-Oct-2009 |
nipkow <none@none> |
Inv -> inv_onto, inv abbr. inv_onto UNIV.
|
#
35ae4948 |
|
17-Oct-2009 |
nipkow <none@none> |
added the_inv_onto
|
#
1e5beb93 |
|
29-Sep-2009 |
wenzelm <none@none> |
explicit indication of Unsynchronized.ref;
|
#
2532b0b7 |
|
10-Sep-2009 |
haftmann <none@none> |
early bootstrap of generic transfer procedure
|
#
c54aa2e0 |
|
10-Aug-2009 |
nipkow <none@none> |
new lemma bij_comp
|
#
7411135a |
|
22-Jul-2009 |
haftmann <none@none> |
moved complete_lattice &c. into separate theory --HG-- rename : src/HOL/Set.thy => src/HOL/Complete_Lattice.thy
|
#
fb17b041 |
|
06-Jul-2009 |
haftmann <none@none> |
moved Inductive.myinv to Fun.inv; tuned
|
#
d18d6a07 |
|
22-Jun-2009 |
haftmann <none@none> |
uniformly capitialized names for subdirectories --HG-- rename : src/HOL/Tools/datatype_package/datatype.ML => src/HOL/Tools/Datatype/datatype.ML rename : src/HOL/Tools/datatype_package/datatype_abs_proofs.ML => src/HOL/Tools/Datatype/datatype_abs_proofs.ML rename : src/HOL/Tools/datatype_package/datatype_aux.ML => src/HOL/Tools/Datatype/datatype_aux.ML rename : src/HOL/Tools/datatype_package/datatype_case.ML => src/HOL/Tools/Datatype/datatype_case.ML rename : src/HOL/Tools/datatype_package/datatype_codegen.ML => src/HOL/Tools/Datatype/datatype_codegen.ML rename : src/HOL/Tools/datatype_package/datatype_prop.ML => src/HOL/Tools/Datatype/datatype_prop.ML rename : src/HOL/Tools/datatype_package/datatype_realizer.ML => src/HOL/Tools/Datatype/datatype_realizer.ML rename : src/HOL/Tools/datatype_package/datatype_rep_proofs.ML => src/HOL/Tools/Datatype/datatype_rep_proofs.ML rename : src/HOL/Tools/function_package/auto_term.ML => src/HOL/Tools/Function/auto_term.ML rename : src/HOL/Tools/function_package/context_tree.ML => src/HOL/Tools/Function/context_tree.ML rename : src/HOL/Tools/function_package/decompose.ML => src/HOL/Tools/Function/decompose.ML rename : src/HOL/Tools/function_package/descent.ML => src/HOL/Tools/Function/descent.ML rename : src/HOL/Tools/function_package/fundef.ML => src/HOL/Tools/Function/fundef.ML rename : src/HOL/Tools/function_package/fundef_common.ML => src/HOL/Tools/Function/fundef_common.ML rename : src/HOL/Tools/function_package/fundef_core.ML => src/HOL/Tools/Function/fundef_core.ML rename : src/HOL/Tools/function_package/fundef_datatype.ML => src/HOL/Tools/Function/fundef_datatype.ML rename : src/HOL/Tools/function_package/fundef_lib.ML => src/HOL/Tools/Function/fundef_lib.ML rename : src/HOL/Tools/function_package/induction_scheme.ML => src/HOL/Tools/Function/induction_scheme.ML rename : src/HOL/Tools/function_package/inductive_wrap.ML => src/HOL/Tools/Function/inductive_wrap.ML rename : src/HOL/Tools/function_package/lexicographic_order.ML => src/HOL/Tools/Function/lexicographic_order.ML rename : src/HOL/Tools/function_package/measure_functions.ML => src/HOL/Tools/Function/measure_functions.ML rename : src/HOL/Tools/function_package/mutual.ML => src/HOL/Tools/Function/mutual.ML rename : src/HOL/Tools/function_package/pattern_split.ML => src/HOL/Tools/Function/pattern_split.ML rename : src/HOL/Tools/function_package/scnp_reconstruct.ML => src/HOL/Tools/Function/scnp_reconstruct.ML rename : src/HOL/Tools/function_package/scnp_solve.ML => src/HOL/Tools/Function/scnp_solve.ML rename : src/HOL/Tools/function_package/size.ML => src/HOL/Tools/Function/size.ML rename : src/HOL/Tools/function_package/sum_tree.ML => src/HOL/Tools/Function/sum_tree.ML rename : src/HOL/Tools/function_package/termination.ML => src/HOL/Tools/Function/termination.ML rename : src/Tools/code/code_haskell.ML => src/Tools/Code/code_haskell.ML rename : src/Tools/code/code_ml.ML => src/Tools/Code/code_ml.ML rename : src/Tools/code/code_preproc.ML => src/Tools/Code/code_preproc.ML rename : src/Tools/code/code_printer.ML => src/Tools/Code/code_printer.ML rename : src/Tools/code/code_target.ML => src/Tools/Code/code_target.ML rename : src/Tools/code/code_thingol.ML => src/Tools/Code/code_thingol.ML
|
#
733ca04e |
|
10-Jun-2009 |
haftmann <none@none> |
separate directory for datatype package --HG-- rename : src/HOL/Tools/datatype_abs_proofs.ML => src/HOL/Tools/datatype_package/datatype_abs_proofs.ML rename : src/HOL/Tools/datatype_case.ML => src/HOL/Tools/datatype_package/datatype_case.ML rename : src/HOL/Tools/datatype_codegen.ML => src/HOL/Tools/datatype_package/datatype_codegen.ML rename : src/HOL/Tools/datatype_package.ML => src/HOL/Tools/datatype_package/datatype_package.ML rename : src/HOL/Tools/datatype_prop.ML => src/HOL/Tools/datatype_package/datatype_prop.ML rename : src/HOL/Tools/datatype_realizer.ML => src/HOL/Tools/datatype_package/datatype_realizer.ML rename : src/HOL/Tools/datatype_rep_proofs.ML => src/HOL/Tools/datatype_package/datatype_rep_proofs.ML
|
#
41260d9c |
|
04-Jun-2009 |
nipkow <none@none> |
A few finite lemmas
|
#
c42bd7f5 |
|
19-May-2009 |
haftmann <none@none> |
pretty printing of functional combinators for evaluation code
|
#
6ca1bd25 |
|
08-May-2009 |
nipkow <none@none> |
lemmas by Andreas Lochbihler
|
#
e295cac3 |
|
05-Mar-2009 |
haftmann <none@none> |
dropped Id
|
#
7e4fc946 |
|
31-Oct-2008 |
berghofe <none@none> |
Replaced arbitrary by undefined.
|
#
d63044b5 |
|
09-Oct-2008 |
haftmann <none@none> |
`code func` now just `code`
|
#
eeba5bb1 |
|
23-Jun-2008 |
wenzelm <none@none> |
Logic.all/mk_equals/mk_implies;
|
#
8c735da8 |
|
13-Jun-2008 |
nipkow <none@none> |
hide -> hide (open)
|
#
f42f96c3 |
|
12-Jun-2008 |
nipkow <none@none> |
Hid swap
|
#
47606962 |
|
10-Jun-2008 |
wenzelm <none@none> |
tuned proofs -- case_tac *is* available here;
|
#
8a6cac34 |
|
10-Jun-2008 |
haftmann <none@none> |
removed some dubious code lemmas
|
#
9878f4e8 |
|
09-Apr-2008 |
haftmann <none@none> |
removed syntax from monad combinators; renamed mbind to scomp
|
#
cee58604 |
|
19-Mar-2008 |
haftmann <none@none> |
added forward composition
|
#
bd98015c |
|
19-Mar-2008 |
wenzelm <none@none> |
more antiquotations;
|
#
bd15820d |
|
26-Feb-2008 |
haftmann <none@none> |
moved some set lemmas to Set.thy
|
#
8510f743 |
|
21-Feb-2008 |
nipkow <none@none> |
moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas, and added some
|
#
27d3ec8c |
|
10-Jan-2008 |
berghofe <none@none> |
Added test data generator for function type (from Pure/codegen.ML).
|
#
35ae3509 |
|
14-Aug-2007 |
paulson <none@none> |
ATP blacklisting is now in theory data, attribute noatp
|
#
981b3ecc |
|
28-Jul-2007 |
wenzelm <none@none> |
simproc_setup fun_upd2;
|
#
b8ec8316 |
|
20-Jul-2007 |
haftmann <none@none> |
simplified HOL bootstrap
|
#
739b482e |
|
11-Jul-2007 |
berghofe <none@none> |
Added ML bindings for sup_fun_eq and sup_bool_eq.
|
#
a140f07e |
|
08-May-2007 |
haftmann <none@none> |
moved recfun_codegen.ML to Code_Generator.thy
|
#
8d82473b |
|
06-May-2007 |
haftmann <none@none> |
changed code generator invocation syntax
|
#
167fea11 |
|
20-Apr-2007 |
haftmann <none@none> |
Isar definitions are now added explicitly to code theorem table
|
#
3f2790ae |
|
03-Apr-2007 |
wenzelm <none@none> |
ML antiquotes;
|
#
4a72f290 |
|
16-Mar-2007 |
haftmann <none@none> |
moved lattice instance here
|
#
ecbc5c28 |
|
27-Dec-2006 |
haftmann <none@none> |
explizit serialization for Haskell id
|
#
f0a2045d |
|
18-Dec-2006 |
haftmann <none@none> |
infix syntax for generated code for composition
|
#
3c629eed |
|
27-Nov-2006 |
haftmann <none@none> |
moved order arities for fun and bool to Fun/Orderings
|
#
c8bb6ee6 |
|
13-Nov-2006 |
haftmann <none@none> |
dropped Typedef dependency
|
#
cbb1a051 |
|
07-Nov-2006 |
wenzelm <none@none> |
renamed 'const_syntax' to 'notation';
|
#
cfdc1311 |
|
07-Jul-2006 |
wenzelm <none@none> |
simprocs: no theory argument -- use simpset context instead;
|
#
61bd82ad |
|
16-May-2006 |
wenzelm <none@none> |
tuned concrete syntax -- abbreviation/const_syntax;
|
#
78ccf652 |
|
02-May-2006 |
wenzelm <none@none> |
replaced syntax/translations by abbreviation;
|
#
b5d7d8ec |
|
08-Apr-2006 |
wenzelm <none@none> |
refined 'abbreviation';
|
#
84161ae1 |
|
23-Mar-2006 |
nipkow <none@none> |
Converted translations to abbbreviations. Removed a few odd functions from Map and AssocList. Moved chg_map from Map to Bali/Basis.
|
#
6e9a9dec |
|
10-Nov-2005 |
huffman <none@none> |
add header
|
#
8cceae71 |
|
21-Oct-2005 |
wenzelm <none@none> |
Goal.prove;
|
#
46e4168a |
|
17-Oct-2005 |
wenzelm <none@none> |
Simplifier.inherit_context instead of Simplifier.inherit_bounds;
|
#
0789ab36 |
|
22-Sep-2005 |
nipkow <none@none> |
renamed rules to iprover
|
#
fff82f5e |
|
16-Aug-2005 |
paulson <none@none> |
classical rules must have names for ATP integration
|
#
678cd7d2 |
|
01-Aug-2005 |
wenzelm <none@none> |
simprocs: Simplifier.inherit_bounds;
|
#
9ce84e7b |
|
06-Jul-2005 |
nipkow <none@none> |
linear arithmetic now takes "&" in assumptions apart.
|
#
bf3fe264 |
|
10-Apr-2005 |
nipkow <none@none> |
_(_|_) is now override_on
|
#
3dffd254 |
|
13-Feb-2005 |
skalberg <none@none> |
Deleted Library.option type.
|
#
a0c5c7ad |
|
09-Feb-2005 |
paulson <none@none> |
new foldSet proofs
|
#
657298fd |
|
13-Jan-2005 |
nipkow <none@none> |
made diff_less a simp rule
|
#
3f348152 |
|
21-Nov-2004 |
nipkow <none@none> |
added lemmas
|
#
0fe1d442 |
|
18-Aug-2004 |
nipkow <none@none> |
import -> imports
|
#
e61c8d7d |
|
16-Aug-2004 |
nipkow <none@none> |
New theory header syntax.
|
#
f2fa5ea3 |
|
04-Aug-2004 |
nipkow <none@none> |
added some inj_on thms
|
#
cd257618 |
|
14-Apr-2004 |
kleing <none@none> |
use more symbols in HTML output
|
#
2ec67d0a |
|
14-Apr-2003 |
nipkow <none@none> |
Added thms
|
#
b0670e6f |
|
10-Oct-2002 |
berghofe <none@none> |
- Added range_ex1_eq - Removed obsolete theorems inj_o and inj_fun_lemma
|
#
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"
|
#
d722726a |
|
11-Dec-2001 |
wenzelm <none@none> |
oops;
|
#
4075877c |
|
10-Dec-2001 |
wenzelm <none@none> |
bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";
|
#
543684e4 |
|
01-Dec-2001 |
wenzelm <none@none> |
renamed class "term" to "type" (actually "HOL.type");
|
#
b83052f4 |
|
20-Nov-2001 |
wenzelm <none@none> |
got rid of theory Inverse_Image;
|
#
c1694cb4 |
|
08-Nov-2001 |
wenzelm <none@none> |
eliminated old "symbols" syntax, use "xsymbols" instead;
|
#
383d093b |
|
27-Sep-2001 |
wenzelm <none@none> |
eliminated theories "equalities" and "mono" (made part of "Typedef", which supercedes "subset");
|
#
03dad649 |
|
25-Jul-2001 |
paulson <none@none> |
partial restructuring to reduce dependence on Axiom of Choice
|
#
175f5605 |
|
14-Feb-2001 |
oheimb <none@none> |
removed whitespace
|
#
b8811f5a |
|
07-Jan-2001 |
nipkow <none@none> |
Removed Applyall
|
#
bc286955 |
|
12-Oct-2000 |
nipkow <none@none> |
*** empty log message ***
|
#
c902e600 |
|
16-Jul-2000 |
wenzelm <none@none> |
syntax (symbols) "op o" moved from HOL to Fun;
|
#
d4ed4f0a |
|
14-Jul-2000 |
oheimb <none@none> |
added hint on fun_sum
|
#
6eb395f6 |
|
13-Jul-2000 |
wenzelm <none@none> |
fixed compose decl;
|
#
e511a500 |
|
25-Jun-2000 |
wenzelm <none@none> |
tuned;
|
#
89a67019 |
|
24-May-2000 |
paulson <none@none> |
we must not require SetInterval this early
|
#
05724178 |
|
22-May-2000 |
nipkow <none@none> |
Added SetInterval
|
#
bba1acb1 |
|
18-Feb-2000 |
oheimb <none@none> |
changed precedence of function update
|
#
1e39b9fd |
|
27-Aug-1999 |
paulson <none@none> |
the bij predicate (at last)
|
#
fb5655ea |
|
03-Feb-1999 |
paulson <none@none> |
inj is now a translation of inj_on
|
#
72480849 |
|
13-Nov-1998 |
paulson <none@none> |
the function space operator
|
#
5ef6afb1 |
|
02-Oct-1998 |
nipkow <none@none> |
id <-> Id
|
#
791a9fe0 |
|
12-Aug-1998 |
oheimb <none@none> |
cleanup for Fun.thy: merged Update.{thy|ML} into Fun.{thy|ML} moved o_def from HOL.thy to Fun.thy added Id_def to Fun.thy moved image_compose from Set.ML to Fun.ML moved o_apply and o_assoc from simpdata.ML to Fun.ML moved fun_upd_same and fun_upd_other (from Map.ML) to Fun.ML added fun_upd_twist to Fun.ML
|
#
e974532e |
|
27-Apr-1998 |
nipkow <none@none> |
Added a few lemmas. Renamed expand_const -> split_const.
|
#
829b854b |
|
24-Feb-1998 |
paulson <none@none> |
New theory of the inverse image of a function
|
#
2e81fd2d |
|
31-Oct-1997 |
paulson <none@none> |
New Blast_tac (and minor tidying...)
|
#
8bb0e87a |
|
04-Apr-1997 |
nipkow <none@none> |
moved inj and surj from Set to Fun and Inv -> inv.
|
#
1d43e2fa |
|
05-Feb-1996 |
clasohm <none@none> |
expanded tabs; renamed subtype to typedef; incorporated Konrad's changes
|
#
46f10ec6 |
|
02-Mar-1995 |
clasohm <none@none> |
new version of HOL with curried function application
|