#
c5b95729 |
|
08-Mar-2020 |
haftmann <none@none> |
more frugal simp rules for bit operations; more pervasive use of bit selector --HG-- extra : rebase_source : 09f56fd30f4ab8ae84811041575772264eb330b3
|
#
a1a97176 |
|
09-Feb-2020 |
haftmann <none@none> |
rule concerning bit (push_bit ...)
|
#
fb14e7d9 |
|
01-Feb-2020 |
haftmann <none@none> |
more specific class assumptions
|
#
f3b05a1f |
|
02-Dec-2019 |
haftmann <none@none> |
tuned material --HG-- extra : rebase_source : 28017ca9e3c54a758db0e8c3ac45e1c2b31b6f65
|
#
57769df1 |
|
01-Dec-2019 |
haftmann <none@none> |
characterization of singleton bit operation
|
#
936f4b2b |
|
17-Nov-2019 |
haftmann <none@none> |
strengthened type class for bit operations
|
#
3b6cecbe |
|
09-Nov-2019 |
haftmann <none@none> |
bit shifts as class operations
|
#
927141b3 |
|
23-Oct-2019 |
haftmann <none@none> |
tuned syntax
|
#
6ee2be1e |
|
14-Jun-2019 |
haftmann <none@none> |
slightly more specialized name for type class
|
#
3431ca3d |
|
30-Mar-2019 |
haftmann <none@none> |
irrelevant --HG-- extra : rebase_source : fff50fd15be0f5d17aa176677f7d646cc5e44265
|
#
ab0f6a9e |
|
28-Mar-2019 |
wenzelm <none@none> |
"export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports; "export_code ... file" is legacy, the empty name form has been discontinued; updated examples;
|
#
4d664052 |
|
22-Mar-2019 |
haftmann <none@none> |
improved code equations taken over from AFP
|
#
a7c0e049 |
|
10-Mar-2019 |
haftmann <none@none> |
migrated from Nums to Zarith as library for OCaml integer arithmetic --HG-- extra : rebase_source : 9da06716fa2cece20a04b2b74f042738c493e925
|
#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
3a4a7136 |
|
24-Apr-2018 |
haftmann <none@none> |
proper datatype for 8-bit characters
|
#
79b69ae3 |
|
20-Apr-2018 |
haftmann <none@none> |
algebraic embeddings for bit operations
|
#
bef5ff04 |
|
20-Mar-2018 |
haftmann <none@none> |
generalized
|
#
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
#
b86a8c59 |
|
03-Jan-2018 |
blanchet <none@none> |
kill old size infrastructure
|
#
aab0bfb7 |
|
19-Oct-2017 |
haftmann <none@none> |
added lemmas and tuned proofs --HG-- extra : rebase_source : 96f42feb3c60e71f2655c97d331ac68baf8b4a63
|
#
2c72473b |
|
09-Oct-2017 |
haftmann <none@none> |
clarified parity --HG-- extra : rebase_source : 7e46e7dfc0f09316c589babeb5a372aeff091071
|
#
f93a9d94 |
|
09-Oct-2017 |
haftmann <none@none> |
clarified uniqueness criterion for euclidean rings --HG-- extra : rebase_source : 3f8d28b5e69282e9e5f36f72ad0d4d2e551ca7ab
|
#
eda74618 |
|
09-Oct-2017 |
haftmann <none@none> |
tuned imports --HG-- extra : rebase_source : bc9797cb892085195c2d8662a7ca3896dd1e5011
|
#
fd2471a9 |
|
08-Oct-2017 |
haftmann <none@none> |
euclidean rings need no normalization --HG-- extra : rebase_source : 7f2e3f676b513d6c59f526f099be30240183bf05
|
#
de79d13d |
|
08-Oct-2017 |
haftmann <none@none> |
one uniform type class for parity structures --HG-- extra : rebase_source : edf12af006cee8d114754f4a1916094166004337
|
#
2ef94418 |
|
08-Oct-2017 |
haftmann <none@none> |
abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel --HG-- extra : rebase_source : c6612d6016d811043143eafb7a671631287494a1
|
#
ad36577d |
|
08-Oct-2017 |
haftmann <none@none> |
avoid fact name clashes --HG-- extra : rebase_source : dadb340e6deb1d95749a6828999b5295bffc7702
|
#
89bed399 |
|
24-Jun-2017 |
haftmann <none@none> |
more direct construction of integer_of_num; code equations for integer_of_char may rely on pattern matching on Char --HG-- extra : rebase_source : 40a2196ad040f66707469d6b3d1be2b7a4b1dc68
|
#
cf03d18a |
|
06-Feb-2017 |
haftmann <none@none> |
computation preprocessing rules to allow literals as input for computations
|
#
ef5da5a8 |
|
09-Jan-2017 |
haftmann <none@none> |
slightly generalized type class hierarchy concerning unit factors, to allow for lean polynomial normalization --HG-- extra : rebase_source : 0d5af77e2a7d66625c22923a19c456b1ca17652e
|
#
40424ca4 |
|
17-Dec-2016 |
haftmann <none@none> |
more fine-grained type class hierarchy for div and mod --HG-- extra : rebase_source : fffbeef99e834ca17596f478178e94bed8a014bc
|
#
4b713e59 |
|
16-Oct-2016 |
haftmann <none@none> |
eliminated irregular aliasses
|
#
e162d30e |
|
16-Oct-2016 |
haftmann <none@none> |
transfer rules for divides relation on integer and natural
|
#
70525112 |
|
12-Oct-2016 |
haftmann <none@none> |
transfer lifting rule for numeral --HG-- extra : rebase_source : bafc2cb3fd6a49a365472e2fb15a4de692ec874d
|
#
3c2b07e1 |
|
25-Sep-2016 |
haftmann <none@none> |
syntactic type class for operation mod named after mod; simplified assumptions of type class semiring_div --HG-- extra : rebase_source : 3714be7474835787b2a513b731c9864d1ac9d2c4
|
#
6989cd63 |
|
29-May-2016 |
haftmann <none@none> |
do not export abstract constructors in code_reflect
|
#
9c074391 |
|
18-Dec-2015 |
Andreas Lochbihler <none@none> |
add serialisation for abs on integer to target language operation
|
#
fb457287 |
|
27-Sep-2015 |
haftmann <none@none> |
monomorphization of divmod wrt. code generation avoids costly dictionary unpacking at runtime --HG-- extra : rebase_source : e05d79a48b81d6ffe67aca3743dbab1781bd1e4f
|
#
62649664 |
|
27-Sep-2015 |
haftmann <none@none> |
more selective preprocessing allows bare "numeral" occurences to be retained as real function in generated code --HG-- extra : rebase_source : ac120f7c610071f077b4f216c87e32c562d227fc
|
#
85ed9565 |
|
01-Sep-2015 |
wenzelm <none@none> |
eliminated \<Colon>;
|
#
e27e1a18 |
|
08-Aug-2015 |
haftmann <none@none> |
direct bootstrap of integer division from natural division
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
456b0fa3 |
|
23-Jun-2015 |
paulson <lp15@cam.ac.uk> |
Amalgamation of the class comm_semiring_1_diff_distrib into comm_semiring_1_cancel. Moving axiom le_add_diff_inverse2 from semiring_numeral_div to linordered_semidom.
|
#
f2ba2c03 |
|
01-Jun-2015 |
haftmann <none@none> |
separate class for division operator, with particular syntax added in more specific classes
|
#
8c67c983 |
|
23-Mar-2015 |
haftmann <none@none> |
distributivity of partial minus establishes desired properties of dvd in semirings --HG-- extra : rebase_source : 99dad957de0410b3a1ca21ff1f8723495b31194f
|
#
d1684c4b |
|
06-Feb-2015 |
haftmann <none@none> |
default abstypes and default abstract equations make technical (no_code) annotation superfluous --HG-- extra : rebase_source : d54bb7382702f44984b3e0e4b39bf01c86d63963
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
5f477322 |
|
18-Sep-2014 |
haftmann <none@none> |
always annotate potentially polymorphic Haskell numerals --HG-- extra : rebase_source : afdd470c78d704a706fe6d34761f4251b2b79ec0
|
#
6fba1337 |
|
18-Sep-2014 |
haftmann <none@none> |
tuned --HG-- extra : rebase_source : f392005c56c1d890fea707e658b1e35131f31bf9
|
#
f81a74f2 |
|
19-Sep-2014 |
blanchet <none@none> |
keep obsolete interpretations in Main, to avoid merge trouble
|
#
22e6cafc |
|
18-Sep-2014 |
blanchet <none@none> |
reintroduced an instantiation of 'size' for 'numerals'
|
#
9b903e0e |
|
18-Sep-2014 |
blanchet <none@none> |
moved old 'size' generator together with 'old_datatype' --HG-- rename : src/HOL/Tools/Function/old_size.ML => src/HOL/Tools/Old_Datatype/old_size.ML
|
#
cb40fd66 |
|
11-Sep-2014 |
blanchet <none@none> |
renamed 'rep_datatype' to 'old_rep_datatype' (HOL)
|
#
e46c07fd |
|
04-Jul-2014 |
haftmann <none@none> |
reduced name variants for assoc and commute on plus and mult
|
#
b3e5b66d |
|
04-May-2014 |
blanchet <none@none> |
renamed 'xxx_size' to 'size_xxx' for old datatype package
|
#
b9ba5739 |
|
06-Mar-2014 |
blanchet <none@none> |
renamed 'fun_rel' to 'rel_fun'
|
#
c567c4b9 |
|
25-Feb-2014 |
kuncar <none@none> |
unregister lifting setup following the best practice of Lifting
|
#
dd44ffb4 |
|
20-Feb-2014 |
blanchet <none@none> |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
#
386379a7 |
|
12-Feb-2014 |
Andreas Lochbihler <none@none> |
make integer_of_char and char_of_integer work with NBE and code_simp
|
#
34a0be19 |
|
12-Feb-2014 |
blanchet <none@none> |
adapted theories to 'xxx_case' to 'case_xxx' * * * 'char_case' -> 'case_char' and same for 'rec' * * * compile * * * renamed 'xxx_case' to 'case_xxx'
|
#
63970edd |
|
12-Feb-2014 |
blanchet <none@none> |
renamed '{prod,sum,bool,unit}_case' to 'case_...'
|
#
138816de |
|
19-Nov-2013 |
haftmann <none@none> |
eliminiated neg_numeral in favour of - (numeral _)
|
#
cb604eb5 |
|
18-Aug-2013 |
haftmann <none@none> |
execution of int division by class semiring_numeral_div, replacing pdivmod by divmod_abs
|
#
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
|
#
3e084fa1 |
|
08-Mar-2013 |
kuncar <none@none> |
patch Isabelle ditribution to conform to changes regarding the parametricity
|
#
5a8927d0 |
|
15-Feb-2013 |
haftmann <none@none> |
two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one --HG-- extra : rebase_source : ffa0242ad108fe680ff144a716257c0784285d17
|
#
d9333ba5 |
|
19-Oct-2012 |
webertj <none@none> |
Renamed {left,right}_distrib to distrib_{right,left}.
|
#
c82bd4c5 |
|
12-Oct-2012 |
wenzelm <none@none> |
discontinued obsolete typedef (open) syntax;
|
#
f59ab713 |
|
23-Jul-2012 |
haftmann <none@none> |
restrict unqualified imports from Haskell Prelude to a small set of fundamental operations
|
#
2a20d32d |
|
01-Apr-2012 |
huffman <none@none> |
removed Nat_Numeral.thy, moving all theorems elsewhere
|
#
8bb6233a |
|
25-Mar-2012 |
huffman <none@none> |
merged fork with new numeral representation (see NEWS)
|
#
484c9d58 |
|
24-Feb-2012 |
haftmann <none@none> |
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy --HG-- extra : rebase_source : ed15629634477aff0a8efea30547f496c70907ad
|
#
37822d49 |
|
23-Feb-2012 |
haftmann <none@none> |
moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy
|
#
efe90bdd |
|
19-Feb-2012 |
huffman <none@none> |
use qualified constant names instead of suffixes (from Florian Haftmann)
|
#
5a9dcbd3 |
|
29-Dec-2011 |
haftmann <none@none> |
attribute code_abbrev superseedes code_unfold_post --HG-- extra : rebase_source : c121dde677a8fb25289c668f8f6a123174fb117d
|
#
d8e74f87 |
|
30-Nov-2011 |
wenzelm <none@none> |
prefer typedef without extra definition and alternative name; tuned proofs;
|
#
363c25c4 |
|
07-Sep-2011 |
huffman <none@none> |
avoid using legacy theorem names
|
#
cac3fde2 |
|
01-Oct-2010 |
haftmann <none@none> |
use module integer for Eval
|
#
40bdb407 |
|
10-Sep-2010 |
haftmann <none@none> |
Haskell == is infix, not infixl
|
#
972f5d58 |
|
27-Aug-2010 |
haftmann <none@none> |
renamed class/constant eq to equal; tuned some instantiations
|
#
1ad44b2b |
|
24-Jul-2010 |
haftmann <none@none> |
another refinement chapter in the neverending numeral story
|
#
759f300c |
|
23-Jul-2010 |
haftmann <none@none> |
avoid unreliable Haskell Int type
|
#
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;
|
#
508e5844 |
|
31-Mar-2010 |
bulwahn <none@none> |
adding iterate_upto interface in compilations and iterate_upto functions in Isabelle theories for arithmetic setup of the predicate compiler
|
#
1d18f590 |
|
10-Mar-2010 |
haftmann <none@none> |
tuned whitespace
|
#
5d17693c |
|
05-Feb-2010 |
haftmann <none@none> |
more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
|
#
a22630a8 |
|
22-Jan-2010 |
haftmann <none@none> |
code literals: distinguish numeral classes by different entries
|
#
499bb143 |
|
14-Jan-2010 |
haftmann <none@none> |
allow individual printing of numerals during code serialization
|
#
df118eed |
|
13-Jan-2010 |
haftmann <none@none> |
some syntax setup for Scala
|
#
f94fe110 |
|
10-Jan-2010 |
berghofe <none@none> |
Adapted to changes in induct method.
|
#
66432170 |
|
29-Oct-2009 |
haftmann <none@none> |
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
|
#
7d4dc9b8 |
|
29-Oct-2009 |
haftmann <none@none> |
moved Nat_Transfer before Divides; distributed Nat_Transfer setup accordingly
|
#
0f96c7cc |
|
28-Oct-2009 |
haftmann <none@none> |
moved theory Divides after theory Nat_Numeral; tuned some proof texts
|
#
5c2bc460 |
|
14-Jul-2009 |
haftmann <none@none> |
prefer code_inline over code_unfold; use code_unfold_post where appropriate
|
#
fbe41aef |
|
14-Jul-2009 |
haftmann <none@none> |
code attributes use common underscore convention
|
#
ed582d00 |
|
02-Jun-2009 |
haftmann <none@none> |
OCaml builtin intergers are elusive; avoid
|
#
14d40ef9 |
|
27-May-2009 |
haftmann <none@none> |
added lemma about 0 - 1
|
#
71924e3c |
|
19-May-2009 |
haftmann <none@none> |
String.literal replaces message_string, code_numeral replaces (code_)index --HG-- rename : src/HOL/Code_Index.thy => src/HOL/Code_Numeral.thy
|