#
eb0bba70 |
|
04-Apr-2019 |
paulson <lp15@cam.ac.uk> |
More group theory. Sum and product indexed by the non-neutral part of a set
|
#
e96f8dee |
|
27-Mar-2019 |
paulson <lp15@cam.ac.uk> |
more stuff from HOL Light: Euclidean spaces and n-spheres, Hausdorff spaces, etc.
|
#
b0924e81 |
|
21-Mar-2019 |
paulson <lp15@cam.ac.uk> |
new material on topology: products, etc. Some renamings, esp continuous_on_topo -> continuous_map
|
#
091484f9 |
|
19-Mar-2019 |
paulson <lp15@cam.ac.uk> |
new material about topology, etc.; also fixes for yesterday's
|
#
6ce8882b |
|
14-Mar-2019 |
wenzelm <none@none> |
more specific keyword kinds;
|
#
e60cf64d |
|
06-Jan-2019 |
wenzelm <none@none> |
isabelle update -u path_cartouches;
|
#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
ec8d5b30 |
|
10-Nov-2018 |
haftmann <none@none> |
clarified status of legacy input abbreviations
|
#
5abaa1a1 |
|
17-Oct-2018 |
paulson <lp15@cam.ac.uk> |
new theory Abstract_Topology with lots of stuff from HOL Light's metric.sml
|
#
e8e7e258 |
|
18-Jun-2018 |
paulson <lp15@cam.ac.uk> |
fixing overloading problems involving vector cross products
|
#
64ccdb76 |
|
17-Jun-2018 |
nipkow <none@none> |
added simp rule
|
#
0043cce7 |
|
08-Feb-2018 |
nipkow <none@none> |
tuned
|
#
5385dbfa |
|
16-Jan-2018 |
wenzelm <none@none> |
standardized towards new-style formal comments: isabelle update_comments;
|
#
9322bd71 |
|
02-Jul-2017 |
haftmann <none@none> |
proper concept of code declaration wrt. atomicity and Isar declarations --HG-- extra : rebase_source : adb08da85e01b6c9c81d471a0d8e7ebb68d7e472
|
#
8806de60 |
|
01-Aug-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
#
ee163328 |
|
29-Jul-2016 |
wenzelm <none@none> |
more accurate cong del; tuned proofs;
|
#
b78a0c93 |
|
05-Jul-2016 |
wenzelm <none@none> |
misc tuning and modernization;
|
#
5339f05b |
|
05-Jul-2016 |
wenzelm <none@none> |
more antiquotations;
|
#
2f8726ce |
|
06-Jun-2016 |
haftmann <none@none> |
conventional syntax for unit abstractions --HG-- extra : rebase_source : ccf0eecc6d3dc90475d72286dbbc7fb9e0ca6938
|
#
e4b45827 |
|
18-Apr-2016 |
paulson <lp15@cam.ac.uk> |
new theorems about convex hulls, etc.; also, renamed some theorems
|
#
81b459a5 |
|
08-Apr-2016 |
wenzelm <none@none> |
eliminated unused simproc identifier;
|
#
bb975ffe |
|
11-Mar-2016 |
blanchet <none@none> |
generate theorems like 'bool.split_sel'
|
#
259fcfd2 |
|
22-Feb-2016 |
paulson <lp15@cam.ac.uk> |
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
|
#
b8ebe2ac |
|
12-Jan-2016 |
Andreas Lochbihler <none@none> |
add BNF instance for Dlist
|
#
da01cc11 |
|
08-Jan-2016 |
hoelzl <none@none> |
add uniform spaces
|
#
0bfb73b6 |
|
28-Dec-2015 |
wenzelm <none@none> |
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
|
#
7c503729 |
|
27-Dec-2015 |
wenzelm <none@none> |
discontinued ASCII replacement syntax <*>;
|
#
0df376fc |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
3487f527 |
|
11-Nov-2015 |
Andreas Lochbihler <none@none> |
add various lemmas
|
#
d0f876b8 |
|
13-Oct-2015 |
haftmann <none@none> |
restored print translation from a1141fb798ff, to prevent a printing misfit observable using "thm divmod_nat_if" in theory "Divides", with a meagure indication in the comment
|
#
18551fee |
|
13-Oct-2015 |
haftmann <none@none> |
prod_case as canonical name for product type eliminator
|
#
d180dd22 |
|
13-Oct-2015 |
haftmann <none@none> |
moved lemmas
|
#
607ae3e3 |
|
09-Oct-2015 |
wenzelm <none@none> |
discontinued specific HTML syntax;
|
#
c60ceb4a |
|
22-Sep-2015 |
haftmann <none@none> |
effective revert of e6b1236f9b3d: spontaneous eta-contraction happens on the print translation level and can only be suppressed on the print translation level --HG-- extra : rebase_source : 0c30edda36a6811c5cbd091dc3b4c52be9932e44
|
#
e0a30cbb |
|
09-Sep-2015 |
wenzelm <none@none> |
simplified simproc programming interfaces;
|
#
e5110f57 |
|
06-Sep-2015 |
haftmann <none@none> |
tuned notation, proofs, namespace
|
#
7ae03d25 |
|
06-Sep-2015 |
haftmann <none@none> |
obsolete: if case_prod is fully applied, it is printed as proper case expression; eta-contracted variants are read best as "uncurry" combinator
|
#
4930226f |
|
06-Sep-2015 |
haftmann <none@none> |
prefer "uncurry" as canonical name for case distinction on products in combinatorial view
|
#
8856f8aa |
|
06-Sep-2015 |
haftmann <none@none> |
tuned
|
#
51980e9f |
|
06-Sep-2015 |
haftmann <none@none> |
obsolete: all (formally unchecked) examples given in the comments work out of the box as advertised
|
#
2e638f74 |
|
06-Sep-2015 |
haftmann <none@none> |
dropped whitespace leftover from b57df8eecad6
|
#
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
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
b4ae9938 |
|
14-Apr-2015 |
Andreas Lochbihler <none@none> |
add lemmas
|
#
093cea8d |
|
31-Mar-2015 |
wenzelm <none@none> |
clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;
|
#
34035ccd |
|
04-Mar-2015 |
wenzelm <none@none> |
tuned signature -- prefer qualified names;
|
#
b8d56fe6 |
|
10-Feb-2015 |
wenzelm <none@none> |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
|
#
ff53cb2b |
|
13-Nov-2014 |
hoelzl <none@none> |
import general theorems from AFP/Markov_Models
|
#
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;
|
#
233ef912 |
|
30-Oct-2014 |
wenzelm <none@none> |
eliminated aliases;
|
#
f9cb1a7a |
|
29-Oct-2014 |
wenzelm <none@none> |
modernized setup;
|
#
d378bad1 |
|
29-Oct-2014 |
wenzelm <none@none> |
modernized setup;
|
#
21239e65 |
|
29-Sep-2014 |
haftmann <none@none> |
corrected white-space accident
|
#
93986db7 |
|
28-Sep-2014 |
haftmann <none@none> |
tuned
|
#
b0d7f95d |
|
19-Sep-2014 |
blanchet <none@none> |
made new 'primrec' bootstrapping-capable
|
#
cb40fd66 |
|
11-Sep-2014 |
blanchet <none@none> |
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
|
#
bb6226ea |
|
10-Sep-2014 |
haftmann <none@none> |
dropped ineffective print_translation which has never been adjusted to check/uncheck-style case patterns
|
#
caa51abc |
|
06-Sep-2014 |
haftmann <none@none> |
added various facts
|
#
cc5256c1 |
|
04-Sep-2014 |
blanchet <none@none> |
added 'plugins' option to control which hooks are enabled
|
#
6fb4e52a |
|
18-Aug-2014 |
blanchet <none@none> |
reordered some (co)datatype property names for more consistency
|
#
ff957440 |
|
12-Jun-2014 |
haftmann <none@none> |
uniform treatment of trivial unit instances: simplify by default, unfold in code preprocessor
|
#
d8d4a952 |
|
10-Jun-2014 |
Andreas Lochbihler <none@none> |
add type class instances for unit
|
#
312f030c |
|
26-May-2014 |
blanchet <none@none> |
got rid of '=:' squiggly
|
#
e131d18e |
|
20-May-2014 |
nipkow <none@none> |
added unit :: linorder
|
#
f97bff67 |
|
21-Apr-2014 |
haftmann <none@none> |
swap with qualifier; tuned
|
#
d766ca99 |
|
12-Apr-2014 |
haftmann <none@none> |
more operations and lemmas --HG-- extra : rebase_source : 8f5be7e0cdc09c667e66c2cda2c667d4da6e5f73
|
#
5b58306d |
|
09-Apr-2014 |
wenzelm <none@none> |
modernized simproc_setup; modernized theory setup;
|
#
2c8d6176 |
|
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
|
#
462f1580 |
|
13-Mar-2014 |
haftmann <none@none> |
tuned proofs
|
#
8f53ef93 |
|
06-Mar-2014 |
blanchet <none@none> |
renamed 'map_pair' to 'map_prod'
|
#
dd44ffb4 |
|
20-Feb-2014 |
blanchet <none@none> |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
#
8e6ecc59 |
|
13-Feb-2014 |
blanchet <none@none> |
aligned the syntax for 'free_constructors' on the 'datatype_new' and 'codatatype' syntax
|
#
1ae6608b |
|
13-Feb-2014 |
blanchet <none@none> |
renamed 'wrap_free_constructors' to 'free_constructors' (cf. 'functor', 'bnf', etc.)
|
#
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
|
#
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'
|
#
63970edd |
|
12-Feb-2014 |
blanchet <none@none> |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
#
aeb06d74 |
|
12-Feb-2014 |
blanchet <none@none> |
avoid duplicate 'case' definitions by first looking up 'Ctr_Sugar'
|
#
4fc86ba9 |
|
12-Feb-2014 |
blanchet <none@none> |
se 'wrap_free_constructors' to register 'sum' , 'prod', 'unit', 'bool' with their discriminators/selectors * * * cleaner simp/iff sets
|
#
eb5ad205 |
|
05-Dec-2013 |
Andreas Lochbihler <none@none> |
restrict admissibility to non-empty chains to allow more syntax-directed proof rules
|
#
03633065 |
|
18-Oct-2013 |
blanchet <none@none> |
killed most "no_atp", to make Sledgehammer more complete
|
#
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
|
#
ffcd6989 |
|
25-May-2013 |
wenzelm <none@none> |
syntax translations always depend on context;
|
#
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
#
d8ea875e |
|
12-Apr-2013 |
wenzelm <none@none> |
modifiers for classical wrappers operate on Proof.context instead of claset;
|
#
fa669f17 |
|
12-Mar-2013 |
nipkow <none@none> |
extended set comprehension notation with {pttrn : A . P}
|
#
6b8e5a08 |
|
17-Feb-2013 |
haftmann <none@none> |
Sieve of Eratosthenes
|
#
09e81af1 |
|
17-Nov-2012 |
wenzelm <none@none> |
tuned signature;
|
#
22db1436 |
|
16-Nov-2012 |
hoelzl <none@none> |
move theorems to be more generally useable --HG-- extra : rebase_source : c1c0d1f5576f4d469d1b4618663774e2f297a214
|
#
0f438868 |
|
17-Oct-2012 |
bulwahn <none@none> |
moving Pair_inject from legacy and duplicate section to general section, as Pair_inject was considered a duplicate in e8400e31528a by mistake (cf. communication on dev mailing list)
|
#
c82bd4c5 |
|
12-Oct-2012 |
wenzelm <none@none> |
discontinued obsolete typedef (open) syntax;
|
#
34d50597 |
|
10-Oct-2012 |
bulwahn <none@none> |
moving simproc from Finite_Set to more appropriate Product_Type theory
|
#
e3227796 |
|
22-Aug-2012 |
wenzelm <none@none> |
prefer ML_file over old uses;
|
#
109489f9 |
|
24-May-2012 |
wenzelm <none@none> |
tuned proofs;
|
#
be3a5cfd |
|
24-Apr-2012 |
blanchet <none@none> |
added "no_atp"s for extremely prolific, useless facts for ATPs
|
#
870593bf |
|
15-Mar-2012 |
wenzelm <none@none> |
declare command keywords via theory header, including strict checking outside Pure;
|
#
8f33b776 |
|
23-Feb-2012 |
haftmann <none@none> |
tuned whitespace
|
#
98c01e6d |
|
21-Feb-2012 |
haftmann <none@none> |
reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
|
#
9af1cc2e |
|
20-Feb-2012 |
haftmann <none@none> |
tuned whitespace
|
#
4cd57042 |
|
01-Jan-2012 |
haftmann <none@none> |
interaction of set operations for execution and membership predicate --HG-- extra : rebase_source : 88e19fdc682e81ad835b4c75d2758a6cba48e84a
|
#
5a9dcbd3 |
|
29-Dec-2011 |
haftmann <none@none> |
attribute code_abbrev superseedes code_unfold_post --HG-- extra : rebase_source : c121dde677a8fb25289c668f8f6a123174fb117d
|
#
f15c080b |
|
26-Dec-2011 |
haftmann <none@none> |
moved various set operations to theory Set (resp. Product_Type)
|
#
0c441fe9 |
|
30-Nov-2011 |
wenzelm <none@none> |
prefer typedef without alternative name;
|
#
d8e74f87 |
|
30-Nov-2011 |
wenzelm <none@none> |
prefer typedef without extra definition and alternative name; tuned proofs;
|
#
d42d30de |
|
28-Nov-2011 |
nipkow <none@none> |
Hide Product_Type.Times - too precious an identifier
|
#
a495a026 |
|
20-Nov-2011 |
wenzelm <none@none> |
eliminated obsolete "standard";
|
#
b150d9c9 |
|
19-Oct-2011 |
bulwahn <none@none> |
removing old code generator setup of inductive predicates
|
#
6d9753b0 |
|
19-Oct-2011 |
bulwahn <none@none> |
removing old code generator setup for product types
|
#
54c58a18 |
|
18-Oct-2011 |
huffman <none@none> |
hide typedef-generated constants Product_Type.prod and Sum_Type.sum
|
#
15635718 |
|
13-Sep-2011 |
huffman <none@none> |
tuned proofs
|
#
bc193659 |
|
08-Aug-2011 |
huffman <none@none> |
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
|
#
eb0f3940 |
|
17-Jul-2011 |
haftmann <none@none> |
moving UNIV = ... equations to their proper theories
|
#
83552e08 |
|
02-Jul-2011 |
haftmann <none@none> |
install case certificate for If after code_datatype declaration for bool
|
#
8cd5b4bf |
|
29-Jun-2011 |
wenzelm <none@none> |
modernized some simproc setup;
|
#
ae3eeacd |
|
29-Jun-2011 |
wenzelm <none@none> |
modernized some simproc setup;
|
#
eb27e462 |
|
19-Apr-2011 |
wenzelm <none@none> |
eliminated Codegen.mode in favour of explicit argument;
|
#
1c017ad4 |
|
08-Apr-2011 |
wenzelm <none@none> |
explicit structure Syntax_Trans; discontinued old-style constrainAbsC; --HG-- rename : src/Pure/Syntax/syn_trans.ML => src/Pure/Syntax/syntax_trans.ML
|
#
8d01a3ac |
|
06-Apr-2011 |
wenzelm <none@none> |
typed_print_translation: discontinued show_sorts argument;
|
#
6701cdc1 |
|
24-Mar-2011 |
wenzelm <none@none> |
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
|
#
8614cac8 |
|
21-Mar-2011 |
nipkow <none@none> |
fixed a printing problem for bounded quantifiers and bounded set operators in the case of tuples
|
#
47bb2a89 |
|
21-Feb-2011 |
blanchet <none@none> |
renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
|
#
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
|
#
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';
|
#
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
|
#
1ee55808 |
|
03-Dec-2010 |
huffman <none@none> |
theorem names generated by the (rep_)datatype command now have mandatory qualifiers
|
#
b97be2fb |
|
22-Nov-2010 |
hoelzl <none@none> |
Replace surj by abbreviation; remove surj_on.
|
#
9dd2a97f |
|
18-Nov-2010 |
haftmann <none@none> |
map_pair replaces prod_fun
|
#
c5b01ed1 |
|
16-Nov-2010 |
huffman <none@none> |
typedef (open) unit
|
#
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
|
#
bb8268b1 |
|
07-Sep-2010 |
nipkow <none@none> |
expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets
|
#
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;
|
#
6cb6c025 |
|
13-Jul-2010 |
bulwahn <none@none> |
correcting function name of generator for products of traditional code generator (introduced in 0040bafffdef)
|
#
55a5de32 |
|
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
|
#
d9e982ba |
|
02-Jul-2010 |
blanchet <none@none> |
adapt Nitpick to "prod_case" and "*" -> "sum" renaming; the code in "Nitpick_Preproc", which sorted the types using "typ_ord", was wrong and evil; it seems to have worked only because "*" was called "*"
|
#
53a0b22e |
|
01-Jul-2010 |
haftmann <none@none> |
"prod" and "sum" replace "*" and "+" respectively
|
#
68b10498 |
|
28-Jun-2010 |
haftmann <none@none> |
merged constants "split" and "prod_case"
|
#
7893b279 |
|
14-Jun-2010 |
haftmann <none@none> |
removed simplifier congruence rule of "prod_case"
|
#
22dc3f97 |
|
09-Jun-2010 |
haftmann <none@none> |
qualified type "*"; qualified constants Pair, fst, snd, split
|
#
07209de2 |
|
08-Jun-2010 |
haftmann <none@none> |
qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
|
#
6ca51413 |
|
01-Jun-2010 |
nipkow <none@none> |
added lemmas
|
#
5405f922 |
|
28-May-2010 |
haftmann <none@none> |
more coherent theory structure; tuned headings
|
#
1d1b0c2b |
|
26-May-2010 |
haftmann <none@none> |
dropped legacy theorem bindings
|
#
23566a86 |
|
04-May-2010 |
krauss <none@none> |
repaired comments where SOMEthing went utterly wrong (cf. 2b04504fcb69)
|
#
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.
|
#
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;
|
#
acdd6b4f |
|
18-Mar-2010 |
haftmann <none@none> |
lemma swap_inj_on, swap_product
|
#
206a5436 |
|
17-Mar-2010 |
blanchet <none@none> |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
#
db258df9 |
|
02-Mar-2010 |
wenzelm <none@none> |
proper (type_)notation;
|
#
4ca307c2 |
|
25-Feb-2010 |
wenzelm <none@none> |
modernized structure Split_Rule; tuned signature; more antiquotations;
|
#
97f02687 |
|
25-Feb-2010 |
wenzelm <none@none> |
more antiquotations;
|
#
4f52a6da |
|
11-Feb-2010 |
wenzelm <none@none> |
modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;
|
#
456c018a |
|
14-Jan-2010 |
haftmann <none@none> |
tuned for products vs. tupled functions
|
#
df118eed |
|
13-Jan-2010 |
haftmann <none@none> |
some syntax setup for Scala
|
#
f124eabb |
|
25-Nov-2009 |
haftmann <none@none> |
bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references) --HG-- extra : rebase_source : f0d460622d846c9dca7630d50d097b93aa8008eb
|
#
f242db1f |
|
12-Nov-2009 |
hoelzl <none@none> |
Renamed upd_snd_conv to apsnd_conv to be consistent with apfst_conv; Added apsnd_apfst_commute
|
#
1d9ca713 |
|
10-Nov-2009 |
haftmann <none@none> |
lemmas about apfst and apsnd
|
#
95b1bd3a |
|
28-Oct-2009 |
haftmann <none@none> |
load Product_Type before Nat; dropped junk
|
#
a9fd0b04 |
|
28-Oct-2009 |
paulson <none@none> |
New theory Probability, which contains a development of measure theory
|
#
ecdd93bf |
|
24-Oct-2009 |
wenzelm <none@none> |
import theory Nat here, which avoids duplicate definition of datatype_realizers (and thus allows to maintain fully authentic fact table);
|
#
75401f7b |
|
15-Oct-2009 |
wenzelm <none@none> |
replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
|
#
a5a5665f |
|
15-Jul-2009 |
wenzelm <none@none> |
more antiquotations;
|
#
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
|
#
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
|
#
a04606c9 |
|
16-Jun-2009 |
haftmann <none@none> |
dropped ID
|
#
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
|
#
c42bd7f5 |
|
19-May-2009 |
haftmann <none@none> |
pretty printing of functional combinators for evaluation code
|
#
8803b7a2 |
|
15-Apr-2009 |
haftmann <none@none> |
default instantiation for unit type
|
#
c9bde67c |
|
20-Mar-2009 |
berghofe <none@none> |
split_codegen now eta-expands terms on-the-fly.
|
#
366aaf8c |
|
06-Nov-2008 |
nipkow <none@none> |
added lemma
|
#
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
|
#
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;
|
#
df0867de |
|
10-Jun-2008 |
haftmann <none@none> |
rep_datatype command now takes list of constructors as input arguments
|
#
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.
|
#
998575ab |
|
07-May-2008 |
berghofe <none@none> |
split_beta is now declared as monotonicity rule, to allow bounded quantifiers in introduction rules of inductive predicates.
|
#
9878f4e8 |
|
09-Apr-2008 |
haftmann <none@none> |
removed syntax from monad combinators; renamed mbind to scomp
|
#
04e92685 |
|
29-Mar-2008 |
wenzelm <none@none> |
replaced 'ML_setup' by 'ML';
|
#
8bf87a62 |
|
19-Mar-2008 |
haftmann <none@none> |
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
|
#
13b177d7 |
|
19-Mar-2008 |
wenzelm <none@none> |
more antiquotations; eliminated change_claset/simpset;
|
#
4174e1a6 |
|
26-Feb-2008 |
bulwahn <none@none> |
Added useful general lemmas from the work with the HeapMonad
|
#
778ab0d7 |
|
10-Jan-2008 |
berghofe <none@none> |
New interface for test data generators.
|
#
55f28d65 |
|
05-Dec-2007 |
haftmann <none@none> |
simplified infrastructure for code generator operational equality
|
#
c7a3ad11 |
|
30-Nov-2007 |
haftmann <none@none> |
more canonical attribute application
|
#
9e0253eb |
|
04-Oct-2007 |
haftmann <none@none> |
certificates for code generator case expressions
|
#
2db87539 |
|
24-Sep-2007 |
haftmann <none@none> |
datatype interpretators for size and datatype_realizer
|
#
35ae3509 |
|
14-Aug-2007 |
paulson <none@none> |
ATP blacklisting is now in theory data, attribute noatp
|
#
0708bd13 |
|
07-Aug-2007 |
haftmann <none@none> |
split off theory Option for benefit of code generator
|
#
146d48fd |
|
05-Jun-2007 |
haftmann <none@none> |
merged Code_Generator.thy into HOL.thy
|
#
a140f07e |
|
08-May-2007 |
haftmann <none@none> |
moved recfun_codegen.ML to Code_Generator.thy
|
#
21289a33 |
|
06-May-2007 |
haftmann <none@none> |
tuned
|
#
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;
|
#
af98260f |
|
12-Mar-2007 |
wenzelm <none@none> |
syntax: proper body priorty for derived binders;
|
#
ea1fde37 |
|
02-Mar-2007 |
haftmann <none@none> |
using "fst" "snd" for Haskell code
|
#
9289470c |
|
23-Feb-2007 |
haftmann <none@none> |
slight cleanup
|
#
1d9f938b |
|
27-Dec-2006 |
haftmann <none@none> |
moved code generator product setup here
|
#
05c1b8f6 |
|
22-Nov-2006 |
haftmann <none@none> |
dropped eq const
|
#
cd65d9bc |
|
16-Nov-2006 |
wenzelm <none@none> |
more robust syntax for definition/abbreviation/notation;
|
#
7a9bd30b |
|
13-Nov-2006 |
haftmann <none@none> |
added thy dependencies
|
#
cbb1a051 |
|
07-Nov-2006 |
wenzelm <none@none> |
renamed 'const_syntax' to 'notation';
|
#
0b0af8f8 |
|
06-Nov-2006 |
haftmann <none@none> |
two further lemmas on split
|
#
2002f725 |
|
16-Oct-2006 |
haftmann <none@none> |
moved HOL code generator setup to Code_Generator
|
#
facb566c |
|
19-Sep-2006 |
haftmann <none@none> |
added operational equality
|
#
72351ae8 |
|
25-Aug-2006 |
paulson <none@none> |
explicit type variables prevent empty sorts
|
#
d8bb4109 |
|
14-Aug-2006 |
haftmann <none@none> |
simplified code generator setup
|
#
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;
|
#
61bd82ad |
|
16-May-2006 |
wenzelm <none@none> |
tuned concrete syntax -- abbreviation/const_syntax;
|
#
1e566d0d |
|
02-May-2006 |
wenzelm <none@none> |
replaced syntax/translations by abbreviation; tuned proofs; tuned;
|
#
b54fe328 |
|
03-Mar-2006 |
nipkow <none@none> |
changed and retracted change of location of code lemmas.
|
#
0a5c5f88 |
|
25-Feb-2006 |
haftmann <none@none> |
improved codegen bootstrap
|
#
4e10cf33 |
|
20-Feb-2006 |
haftmann <none@none> |
slight code generator serialization improvements
|
#
87b39d08 |
|
14-Feb-2006 |
haftmann <none@none> |
added theory of executable rational numbers
|
#
df2fe26f |
|
10-Feb-2006 |
haftmann <none@none> |
improved code generator devarification
|
#
007a22f5 |
|
07-Feb-2006 |
haftmann <none@none> |
slight improvements in code generation
|
#
446dee87 |
|
23-Jan-2006 |
haftmann <none@none> |
removed problematic keyword 'atom'
|
#
75fddbe8 |
|
19-Jan-2006 |
wenzelm <none@none> |
setup: theory -> theory;
|
#
3d5d36c4 |
|
19-Jan-2006 |
berghofe <none@none> |
Re-inserted consts_code declaration accidentally deleted during last commit.
|
#
fe7871ca |
|
17-Jan-2006 |
haftmann <none@none> |
substantial improvements in code generator
|
#
8ce9d893 |
|
29-Dec-2005 |
haftmann <none@none> |
adaptions to changes in code generator
|
#
d2b0060d |
|
08-Dec-2005 |
wenzelm <none@none> |
tuned proofs;
|
#
8394b1b3 |
|
02-Dec-2005 |
haftmann <none@none> |
adjusted to improved code generator interface
|
#
a302a4ce |
|
01-Dec-2005 |
wenzelm <none@none> |
simprocs: static evaluation of simpset;
|
#
d1b7a773 |
|
21-Nov-2005 |
haftmann <none@none> |
added codegenerator
|
#
69d8e2c7 |
|
28-Oct-2005 |
haftmann <none@none> |
added extraction interface for code generator
|
#
8cceae71 |
|
21-Oct-2005 |
wenzelm <none@none> |
Goal.prove;
|
#
f7fba198 |
|
17-Oct-2005 |
wenzelm <none@none> |
change_claset/simpset; Simplifier.inherit_context instead of Simplifier.inherit_bounds;
|
#
c046356e |
|
07-Oct-2005 |
wenzelm <none@none> |
replaced _K by dummy abstraction;
|
#
9dccfecd |
|
16-Aug-2005 |
paulson <none@none> |
more simprules now have names
|
#
781a48c0 |
|
03-Aug-2005 |
berghofe <none@none> |
Fixed bug in code generator for let and split leading to ill-formed code.
|
#
593d5827 |
|
02-Aug-2005 |
wenzelm <none@none> |
simprocs: Simplifier.inherit_bounds;
|
#
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.
|
#
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
#
693b136f |
|
31-May-2005 |
wenzelm <none@none> |
tuned;
|
#
eee46a1e |
|
02-Mar-2005 |
skalberg <none@none> |
Move towards standard functions.
|
#
3dffd254 |
|
13-Feb-2005 |
skalberg <none@none> |
Deleted Library.option type.
|
#
883f343f |
|
01-Feb-2005 |
paulson <none@none> |
the new subst tactic, by Lucas Dixon
|
#
4fb5d159 |
|
18-Dec-2004 |
schirmer <none@none> |
added print translation for split: split f --> %(x,y). f x y
|
#
23b365e5 |
|
13-Dec-2004 |
paulson <none@none> |
removal of NatArith.ML and Product_Type.ML
|
#
7e9454df |
|
10-Dec-2004 |
berghofe <none@none> |
New code generator for let and split.
|
#
0fe1d442 |
|
18-Aug-2004 |
nipkow <none@none> |
import -> imports
|
#
e61c8d7d |
|
16-Aug-2004 |
nipkow <none@none> |
New theory header syntax.
|
#
8e428084 |
|
16-Jun-2004 |
paulson <none@none> |
removal of x-symbol syntax <Sigma> for dependent products
|
#
cd257618 |
|
14-Apr-2004 |
kleing <none@none> |
use more symbols in HTML output
|
#
ea647716 |
|
20-Jan-2004 |
schirmer <none@none> |
Added print translation for pairs
|
#
eade7171 |
|
04-Jan-2004 |
nipkow <none@none> |
undid split_comp_eq[simp] because it leads to nontermination together with split_def!
|
#
b79b3996 |
|
26-Sep-2003 |
paulson <none@none> |
misc tidying
|
#
6259f33a |
|
15-Sep-2003 |
skalberg <none@none> |
Fixed blunder in the setup of the classical reasoner wrt. the constant "curry".
|
#
e6db0639 |
|
14-Sep-2003 |
skalberg <none@none> |
Added the constant "curry".
|
#
f20bcaa2 |
|
11-Jul-2003 |
oheimb <none@none> |
added upd_fst, upd_snd, some thms
|
#
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;
|
#
543684e4 |
|
01-Dec-2001 |
wenzelm <none@none> |
renamed class "term" to "type" (actually "HOL.type");
|
#
c1694cb4 |
|
08-Nov-2001 |
wenzelm <none@none> |
eliminated old "symbols" syntax, use "xsymbols" instead;
|
#
521826c6 |
|
27-Oct-2001 |
wenzelm <none@none> |
tuned;
|
#
a8585515 |
|
19-Oct-2001 |
wenzelm <none@none> |
got rid of ML proof scripts for Product_Type;
|
#
ad5919cf |
|
17-Oct-2001 |
wenzelm <none@none> |
proper proof of split_paired_all (presently unused);
|
#
ad46f14c |
|
15-Oct-2001 |
wenzelm <none@none> |
tuned;
|
#
0faf26eb |
|
27-Sep-2001 |
wenzelm <none@none> |
renamed "()" to Unity, made local;
|
#
eaa9531f |
|
09-Aug-2001 |
oheimb <none@none> |
added pair_imageI (also as intro rule)
|
#
03dad649 |
|
25-Jul-2001 |
paulson <none@none> |
partial restructuring to reduce dependence on Axiom of Choice
|
#
7fdc5d98 |
|
15-Jul-2001 |
wenzelm <none@none> |
tuned;
|
#
8ba0d577 |
|
02-Feb-2001 |
wenzelm <none@none> |
added hidden internal_split constant; tuned;
|
#
29dd0d8a |
|
01-Feb-2001 |
oheimb <none@none> |
converted to Isar therory, adding attributes complete_split and split_format
|
#
21a1484b |
|
23-Oct-2000 |
wenzelm <none@none> |
tuned deps;
|
#
322ec07c |
|
12-Oct-2000 |
nipkow <none@none> |
*** empty log message ***
|