| #
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 ***
|