#
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
|
#
3b6cecbe |
|
09-Nov-2019 |
haftmann <none@none> |
bit shifts as class operations
|
#
6ee2be1e |
|
14-Jun-2019 |
haftmann <none@none> |
slightly more specialized name for type class
|
#
a7c0e049 |
|
10-Mar-2019 |
haftmann <none@none> |
migrated from Nums to Zarith as library for OCaml integer arithmetic --HG-- extra : rebase_source : 9da06716fa2cece20a04b2b74f042738c493e925
|
#
087faccf |
|
08-Mar-2019 |
haftmann <none@none> |
proper code_simp setup for literals --HG-- extra : rebase_source : 419d15d6c51642cd5dc03c383eff3a88eda5f90b
|
#
fc0f183a |
|
25-Jan-2019 |
haftmann <none@none> |
prefer proper strings in OCaml
|
#
e60cf64d |
|
06-Jan-2019 |
wenzelm <none@none> |
isabelle update -u path_cartouches;
|
#
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
25a29bd5 |
|
08-Nov-2018 |
wenzelm <none@none> |
isabelle update_cartouches -t;
|
#
7c43e5f4 |
|
20-May-2018 |
wenzelm <none@none> |
prefer HTTPS;
|
#
11a92088 |
|
25-Apr-2018 |
haftmann <none@none> |
uniform tagging for printable and non-printable literals
|
#
3a4a7136 |
|
24-Apr-2018 |
haftmann <none@none> |
proper datatype for 8-bit characters
|
#
68152afe |
|
26-Feb-2018 |
haftmann <none@none> |
new lemma
|
#
ce7d743d |
|
26-Feb-2018 |
haftmann <none@none> |
dedicated append function for string literals
|
#
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
#
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
#
5a8f249f |
|
02-Aug-2017 |
haftmann <none@none> |
lifting setup for char --HG-- extra : rebase_source : bb7bcf88b2f19b193b28620c0e9a2bb78e69feb4
|
#
9322bd71 |
|
02-Jul-2017 |
haftmann <none@none> |
proper concept of code declaration wrt. atomicity and Isar declarations --HG-- extra : rebase_source : adb08da85e01b6c9c81d471a0d8e7ebb68d7e472
|
#
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
|
#
06aab68a |
|
20-Dec-2016 |
haftmann <none@none> |
emphasize dedicated rewrite rules for congruences --HG-- extra : rebase_source : 28c5807c3eda548e5ed0637459d63997c46e3ff3
|
#
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
|
#
0ced79fe |
|
19-Mar-2016 |
haftmann <none@none> |
unified CHAR with CHR syntax
|
#
8175ce0f |
|
12-Mar-2016 |
haftmann <none@none> |
model characters directly as range 0..255 * * * operate on syntax terms rather than asts
|
#
f318340b |
|
09-Mar-2016 |
haftmann <none@none> |
moved
|
#
204908bc |
|
18-Feb-2016 |
haftmann <none@none> |
more direct bootstrap of char type, still retaining the nibble representation for syntax --HG-- extra : rebase_source : fd206c5addb099b720d632a7511e1485f7f64874
|
#
0df376fc |
|
07-Dec-2015 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
b22e4c0f |
|
07-Oct-2015 |
blanchet <none@none> |
disable generation of 'case_transfer' for 'nibble', due to quadratic proof -- to make 'HOL-Proofs' happier
|
#
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
|
#
cb97119b |
|
27-Jul-2015 |
wenzelm <none@none> |
tuned signature;
|
#
1901affb |
|
18-Jul-2015 |
wenzelm <none@none> |
isabelle update_cartouches;
|
#
a9a5e99e |
|
06-Mar-2015 |
wenzelm <none@none> |
clarified context;
|
#
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
#
103d949b |
|
05-Feb-2015 |
haftmann <none@none> |
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
|
#
2be35839 |
|
05-Feb-2015 |
haftmann <none@none> |
explicit type annotation avoids problems with Haskell type inference
|
#
794edf80 |
|
02-Nov-2014 |
wenzelm <none@none> |
modernized header uniformly as section;
|
#
bd247b58 |
|
29-Oct-2014 |
wenzelm <none@none> |
modernized setup;
|
#
5fc26177 |
|
11-Sep-2014 |
blanchet <none@none> |
updated news
|
#
1ba740de |
|
02-Sep-2014 |
blanchet <none@none> |
use 'datatype_new' in 'Main'
|
#
e46c07fd |
|
04-Jul-2014 |
haftmann <none@none> |
reduced name variants for assoc and commute on plus and mult
|
#
1a78d9f5 |
|
30-Jun-2014 |
haftmann <none@none> |
qualified String.explode and String.implode
|
#
bf47da1c |
|
12-Jun-2014 |
nipkow <none@none> |
added [simp]
|
#
b3e5b66d |
|
04-May-2014 |
blanchet <none@none> |
renamed 'xxx_size' to 'size_xxx' for old datatype package
|
#
c4dc0538 |
|
07-Mar-2014 |
blanchet <none@none> |
use balanced tuples in 'primcorec'
|
#
dd44ffb4 |
|
20-Feb-2014 |
blanchet <none@none> |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
#
208bb532 |
|
12-Feb-2014 |
Andreas Lochbihler <none@none> |
make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
|
#
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'
|
#
de17fb4e |
|
15-Jan-2014 |
wenzelm <none@none> |
added \<newline> symbol, which is used for char/string literals in HOL;
|
#
3bb1b920 |
|
20-Nov-2013 |
Andreas Lochbihler <none@none> |
setup lifting/transfer for String.literal
|
#
d44df382 |
|
09-Oct-2013 |
Andreas Lochbihler <none@none> |
add congruence rule to prevent code_simp from looping
|
#
07f2e82d |
|
08-Aug-2013 |
Andreas Lochbihler <none@none> |
abort execution of generated code with explicit exception message
|
#
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
|
#
50985749 |
|
11-Jun-2013 |
haftmann <none@none> |
reflexive nbe equation for equality on String.literal
|
#
0928b2db |
|
18-Apr-2013 |
wenzelm <none@none> |
simplifier uses proper Proof.context instead of historic type simpset;
|
#
963a5558 |
|
15-Feb-2013 |
haftmann <none@none> |
systematic conversions between nat and nibble/char; more uniform approaches to execute operations on nibble/char --HG-- extra : rebase_source : 982810ecce9e31070e2293715ed744c3b68ae21d
|
#
e455b9c3 |
|
22-Oct-2012 |
haftmann <none@none> |
incorporated constant chars into instantiation proof for enum; tuned proofs for properties on enum of chars; swapped theory dependency of Enum.thy and String.thy
|
#
bbf74aa0 |
|
20-Oct-2012 |
haftmann <none@none> |
moved quite generic material from theory Enum to more appropriate places --HG-- extra : rebase_source : aada8b3ff46b715201e6ecbb53f390c25461ebd9
|
#
c82bd4c5 |
|
12-Oct-2012 |
wenzelm <none@none> |
discontinued obsolete typedef (open) syntax;
|
#
e3227796 |
|
22-Aug-2012 |
wenzelm <none@none> |
prefer ML_file over old uses;
|
#
96682752 |
|
15-Feb-2012 |
wenzelm <none@none> |
renamed "xstr" to "str_token";
|
#
8c33a56f |
|
14-Nov-2011 |
wenzelm <none@none> |
inner syntax positions for string literals;
|
#
b04db96a |
|
19-Oct-2011 |
bulwahn <none@none> |
removing old code generator setup for strings
|
#
7994d347 |
|
18-Aug-2011 |
haftmann <none@none> |
observe distinction between sets and predicates more properly
|
#
7685bb05 |
|
20-Apr-2011 |
wenzelm <none@none> |
discontinuend obsolete Thm.definitionK, which was hardly ever well-defined;
|
#
eb27e462 |
|
19-Apr-2011 |
wenzelm <none@none> |
eliminated Codegen.mode in favour of explicit argument;
|
#
0d0a8a60 |
|
30-Mar-2011 |
bulwahn <none@none> |
renewing specifications in HOL: replacing types by type_synonym
|
#
8080d93b |
|
10-Feb-2011 |
haftmann <none@none> |
reverted cs. 0a3fa8fbcdc5 -- motivation is unreconstructable, produces confusion in user space
|
#
308c65f5 |
|
20-Sep-2010 |
wenzelm <none@none> |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only; --HG-- rename : src/Pure/pure_thy.ML => src/Pure/global_theory.ML
|
#
5b59da77 |
|
13-Sep-2010 |
nipkow <none@none> |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
#
3c66cf8a |
|
10-Sep-2010 |
bulwahn <none@none> |
fiddling with the correct setup for String.literal
|
#
40bdb407 |
|
10-Sep-2010 |
haftmann <none@none> |
Haskell == is infix, not infixl
|
#
003a5bd9 |
|
09-Sep-2010 |
bulwahn <none@none> |
changing String.literal to a type instead of a datatype
|
#
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
|
#
fcf767bf |
|
27-Aug-2010 |
wenzelm <none@none> |
more antiquotations;
|
#
eff6b64f |
|
08-Jul-2010 |
haftmann <none@none> |
tuned module names
|
#
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;
|
#
5404b7b7 |
|
13-Feb-2010 |
wenzelm <none@none> |
modernized structures;
|
#
4f52a6da |
|
11-Feb-2010 |
wenzelm <none@none> |
modernized translations; formal markup of @{syntax_const} and @{const_syntax}; minor tuning;
|
#
df118eed |
|
13-Jan-2010 |
haftmann <none@none> |
some syntax setup for Scala
|
#
cedd9e79 |
|
27-Oct-2009 |
haftmann <none@none> |
tuned
|
#
50da8ae7 |
|
22-Oct-2009 |
haftmann <none@none> |
map_range (and map_index) combinator
|
#
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
|
#
965acf35 |
|
08-Jun-2009 |
haftmann <none@none> |
constant "chars" of all characters
|
#
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
|
#
7f44bec0 |
|
16-May-2009 |
haftmann <none@none> |
is a definition
|
#
155bffcd |
|
16-May-2009 |
bulwahn <none@none> |
added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages
|
#
e1708bd6 |
|
06-May-2009 |
haftmann <none@none> |
proper structures for list and string code generation stuff
|
#
b2241263 |
|
06-May-2009 |
haftmann <none@none> |
refined HOL string theories and corresponding ML fragments
|
#
705e49fd |
|
02-Nov-2001 |
wenzelm <none@none> |
moved into Main;
|
#
cacfa3bb |
|
15-Jan-2001 |
wenzelm <none@none> |
improved string syntax (allow translation rules);
|
#
db8c5d88 |
|
23-Dec-2000 |
wenzelm <none@none> |
Tools/string_syntax.ML;
|
#
888d07b6 |
|
16-Aug-1999 |
wenzelm <none@none> |
'a list: Nil, Cons;
|
#
dba3b50b |
|
17-Mar-1999 |
wenzelm <none@none> |
xstr token class;
|
#
953c4bb8 |
|
03-Jul-1998 |
wenzelm <none@none> |
moved String theory to main HOL;
|