| Sun, 06 Oct 2024 22:56:07 +0200 |
wenzelm |
more inner-syntax markup, without pretty blocks;
|
file |
diff |
annotate
|
| Sat, 05 Oct 2024 22:24:24 +0200 |
wenzelm |
more inner-syntax markup;
|
file |
diff |
annotate
|
| Fri, 04 Oct 2024 13:29:33 +0200 |
wenzelm |
clarified syntax for opening bundles;
|
file |
diff |
annotate
|
| Mon, 23 Sep 2024 13:32:38 +0200 |
wenzelm |
standardize mixfix annotations via "isabelle update -u mixfix_cartouches -l Pure HOL" --- to simplify systematic editing;
|
file |
diff |
annotate
|
| Sun, 25 Aug 2024 15:02:19 +0200 |
wenzelm |
more markup for syntax consts;
|
file |
diff |
annotate
|
| Fri, 05 Apr 2024 21:21:02 +0200 |
wenzelm |
avoid Scala if-expressions and thus make it work both for -new-syntax or -old-syntax;
|
file |
diff |
annotate
|
| Fri, 05 Apr 2024 20:41:54 +0200 |
wenzelm |
proper Scala code for String.literal_of_asciis: avoid ambiguity of ("" ++ ...);
|
file |
diff |
annotate
|
| Sat, 11 Nov 2023 17:44:03 +0000 |
haftmann |
more specific name for type class
|
file |
diff |
annotate
|
| Mon, 25 Jul 2022 06:31:32 +0000 |
haftmann |
Avoid shadowing original List._ namespace.
|
file |
diff |
annotate
|
| Sat, 09 Jul 2022 08:05:53 +0000 |
haftmann |
refined code equations for characters
|
file |
diff |
annotate
|
| Mon, 04 Jul 2022 07:57:22 +0000 |
haftmann |
officical abstract characters for code generation
|
file |
diff |
annotate
|
| Sat, 25 Jun 2022 09:50:37 +0000 |
haftmann |
Centralized some char-related lemmas in distribution.
|
file |
diff |
annotate
|
| Sat, 02 Apr 2022 17:03:34 +0000 |
haftmann |
tuned whitespace in generated code
|
file |
diff |
annotate
|
| Thu, 17 Feb 2022 19:42:15 +0000 |
haftmann |
Avoid overaggresive simplification.
|
file |
diff |
annotate
|
| Mon, 13 Sep 2021 14:18:24 +0000 |
haftmann |
explicit predicate for confined bit range avoids cyclic rewriting in presence of extensionality rule for bit values (contributed by Thomas Sewell)
|
file |
diff |
annotate
|
| Tue, 03 Aug 2021 13:53:22 +0000 |
haftmann |
simplified hierarchy of type classes for bit operations
|
file |
diff |
annotate
|
| Mon, 02 Aug 2021 10:01:06 +0000 |
haftmann |
moved theory Bit_Operations into Main corpus
|
file |
diff |
annotate
|
| Sun, 15 Nov 2020 10:13:03 +0000 |
haftmann |
official collection for bit projection simplifications
|
file |
diff |
annotate
|
| Wed, 19 Aug 2020 12:58:28 +0100 |
paulson |
Another go with lex: now lexordp back in class ord
|
file |
diff |
annotate
|
| Mon, 17 Aug 2020 15:42:38 +0100 |
paulson |
S Holub's proposed generalisation of the lexicographic product of two orderings
|
file |
diff |
annotate
|
| Sat, 11 Jul 2020 18:09:09 +0000 |
haftmann |
a generic horner sum operation
|
file |
diff |
annotate
|
| Fri, 08 May 2020 06:26:28 +0000 |
haftmann |
prefer _ mod 2 over of_bool (odd _)
|
file |
diff |
annotate
|
| Sun, 08 Mar 2020 17:07:49 +0000 |
haftmann |
more frugal simp rules for bit operations; more pervasive use of bit selector
|
file |
diff |
annotate
|
| Sat, 09 Nov 2019 15:39:21 +0000 |
haftmann |
bit shifts as class operations
|
file |
diff |
annotate
|
| Fri, 14 Jun 2019 08:34:27 +0000 |
haftmann |
slightly more specialized name for type class
|
file |
diff |
annotate
|
| Sun, 10 Mar 2019 15:16:45 +0000 |
haftmann |
migrated from Nums to Zarith as library for OCaml integer arithmetic
|
file |
diff |
annotate
|
| Fri, 08 Mar 2019 18:56:48 +0000 |
haftmann |
proper code_simp setup for literals
|
file |
diff |
annotate
|
| Fri, 25 Jan 2019 22:13:48 +0000 |
haftmann |
prefer proper strings in OCaml
|
file |
diff |
annotate
|
| Sun, 06 Jan 2019 15:04:34 +0100 |
wenzelm |
isabelle update -u path_cartouches;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Thu, 08 Nov 2018 22:29:09 +0100 |
wenzelm |
isabelle update_cartouches -t;
|
file |
diff |
annotate
|
| Sun, 20 May 2018 11:57:17 +0200 |
wenzelm |
prefer HTTPS;
|
file |
diff |
annotate
|
| Wed, 25 Apr 2018 09:04:25 +0000 |
haftmann |
uniform tagging for printable and non-printable literals
|
file |
diff |
annotate
|
| Tue, 24 Apr 2018 14:17:58 +0000 |
haftmann |
proper datatype for 8-bit characters
|
file |
diff |
annotate
|
| Mon, 26 Feb 2018 11:52:53 +0000 |
haftmann |
new lemma
|
file |
diff |
annotate
|
| Mon, 26 Feb 2018 11:52:52 +0000 |
haftmann |
dedicated append function for string literals
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Thu, 03 Aug 2017 12:50:03 +0200 |
haftmann |
lifting setup for char
|
file |
diff |
annotate
|
| Sun, 02 Jul 2017 20:13:38 +0200 |
haftmann |
proper concept of code declaration wrt. atomicity and Isar declarations
|
file |
diff |
annotate
|
| Sat, 24 Jun 2017 09:17:35 +0200 |
haftmann |
more direct construction of integer_of_num;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2017 20:56:38 +0100 |
haftmann |
computation preprocessing rules to allow literals as input for computations
|
file |
diff |
annotate
|
| Tue, 20 Dec 2016 15:39:13 +0100 |
haftmann |
emphasize dedicated rewrite rules for congruences
|
file |
diff |
annotate
|
| Mon, 26 Sep 2016 07:56:54 +0200 |
haftmann |
syntactic type class for operation mod named after mod;
|
file |
diff |
annotate
|
| Sat, 19 Mar 2016 16:53:09 +0100 |
haftmann |
unified CHAR with CHR syntax
|
file |
diff |
annotate
|
| Sat, 12 Mar 2016 22:04:52 +0100 |
haftmann |
model characters directly as range 0..255
|
file |
diff |
annotate
|
| Thu, 10 Mar 2016 12:33:01 +0100 |
haftmann |
moved
|
file |
diff |
annotate
|
| Thu, 18 Feb 2016 17:52:52 +0100 |
haftmann |
more direct bootstrap of char type, still retaining the nibble representation for syntax
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Wed, 07 Oct 2015 10:02:43 +0200 |
blanchet |
disable generation of 'case_transfer' for 'nibble', due to quadratic proof -- to make 'HOL-Proofs' happier
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
| Thu, 27 Aug 2015 21:19:48 +0200 |
haftmann |
standardized some occurences of ancient "split" alias
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 17:44:55 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 23:44:51 +0100 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Thu, 05 Feb 2015 19:44:14 +0100 |
haftmann |
slightly more standard code setup for String.literal, with explicit special case in predicate compiler
|
file |
diff |
annotate
|
| Thu, 05 Feb 2015 19:44:13 +0100 |
haftmann |
explicit type annotation avoids problems with Haskell type inference
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Wed, 29 Oct 2014 15:07:53 +0100 |
wenzelm |
modernized setup;
|
file |
diff |
annotate
|
| Thu, 11 Sep 2014 19:32:36 +0200 |
blanchet |
updated news
|
file |
diff |
annotate
|
| Wed, 03 Sep 2014 00:06:24 +0200 |
blanchet |
use 'datatype_new' in 'Main'
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
| Mon, 30 Jun 2014 08:00:36 +0200 |
haftmann |
qualified String.explode and String.implode
|
file |
diff |
annotate
|
| Thu, 12 Jun 2014 18:47:16 +0200 |
nipkow |
added [simp]
|
file |
diff |
annotate
|
| Sun, 04 May 2014 18:14:58 +0200 |
blanchet |
renamed 'xxx_size' to 'size_xxx' for old datatype package
|
file |
diff |
annotate
|
| Fri, 07 Mar 2014 14:21:15 +0100 |
blanchet |
use balanced tuples in 'primcorec'
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 00:09:56 +0100 |
blanchet |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 10:59:25 +0100 |
Andreas Lochbihler |
merged
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:56:38 +0100 |
Andreas Lochbihler |
make lifting setup for String.literal local to prevent transfer from replacing STR ''...'' literals
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:35:57 +0100 |
blanchet |
adapted theories to 'xxx_case' to 'case_xxx'
|
file |
diff |
annotate
|
| Wed, 15 Jan 2014 23:25:28 +0100 |
wenzelm |
added \<newline> symbol, which is used for char/string literals in HOL;
|
file |
diff |
annotate
|
| Wed, 20 Nov 2013 11:10:05 +0100 |
Andreas Lochbihler |
setup lifting/transfer for String.literal
|
file |
diff |
annotate
|
| Wed, 09 Oct 2013 15:33:20 +0200 |
Andreas Lochbihler |
add congruence rule to prevent code_simp from looping
|
file |
diff |
annotate
|
| Thu, 08 Aug 2013 16:10:05 +0200 |
Andreas Lochbihler |
abort execution of generated code with explicit exception message
|
file |
diff |
annotate
|
| Sun, 23 Jun 2013 21:16:07 +0200 |
haftmann |
migration from code_(const|type|class|instance) to code_printing and from code_module to code_identifier
|
file |
diff |
annotate
|
| Tue, 11 Jun 2013 21:07:53 +0200 |
haftmann |
reflexive nbe equation for equality on String.literal
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Fri, 15 Feb 2013 11:47:33 +0100 |
haftmann |
systematic conversions between nat and nibble/char;
|
file |
diff |
annotate
|
| Mon, 22 Oct 2012 22:24:34 +0200 |
haftmann |
incorporated constant chars into instantiation proof for enum;
|
file |
diff |
annotate
|
| Sat, 20 Oct 2012 09:12:16 +0200 |
haftmann |
moved quite generic material from theory Enum to more appropriate places
|
file |
diff |
annotate
|
| Fri, 12 Oct 2012 18:58:20 +0200 |
wenzelm |
discontinued obsolete typedef (open) syntax;
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| Wed, 15 Feb 2012 13:24:22 +0100 |
wenzelm |
renamed "xstr" to "str_token";
|
file |
diff |
annotate
|
| Mon, 14 Nov 2011 17:48:26 +0100 |
wenzelm |
inner syntax positions for string literals;
|
file |
diff |
annotate
|
| Wed, 19 Oct 2011 08:37:29 +0200 |
bulwahn |
removing old code generator setup for strings
|
file |
diff |
annotate
|
| Thu, 18 Aug 2011 13:55:26 +0200 |
haftmann |
observe distinction between sets and predicates more properly
|
file |
diff |
annotate
|
| Thu, 21 Apr 2011 12:56:27 +0200 |
wenzelm |
discontinuend obsolete Thm.definitionK, which was hardly ever well-defined;
|
file |
diff |
annotate
|
| Tue, 19 Apr 2011 23:57:28 +0200 |
wenzelm |
eliminated Codegen.mode in favour of explicit argument;
|
file |
diff |
annotate
|
| Wed, 30 Mar 2011 11:32:52 +0200 |
bulwahn |
renewing specifications in HOL: replacing types by type_synonym
|
file |
diff |
annotate
|
| Thu, 10 Feb 2011 10:32:12 +0100 |
haftmann |
reverted cs. 0a3fa8fbcdc5 -- motivation is unreconstructable, produces confusion in user space
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 16:05:25 +0200 |
wenzelm |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
|
file |
diff |
annotate
|
| Mon, 13 Sep 2010 11:13:15 +0200 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| Fri, 10 Sep 2010 10:59:09 +0200 |
bulwahn |
fiddling with the correct setup for String.literal
|
file |
diff |
annotate
|
| Fri, 10 Sep 2010 10:21:25 +0200 |
haftmann |
Haskell == is infix, not infixl
|
file |
diff |
annotate
|
| Thu, 09 Sep 2010 14:38:14 +0200 |
bulwahn |
changing String.literal to a type instead of a datatype
|
file |
diff |
annotate
|
| Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| Sat, 28 Aug 2010 11:42:33 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 19:34:23 +0200 |
haftmann |
renamed class/constant eq to equal; tuned some instantiations
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 17:59:40 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Thu, 08 Jul 2010 16:19:23 +0200 |
haftmann |
tuned module names
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 21:28:09 +0200 |
wenzelm |
replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
|
file |
diff |
annotate
|
| Sat, 13 Feb 2010 23:24:57 +0100 |
wenzelm |
modernized structures;
|
file |
diff |
annotate
|
| Thu, 11 Feb 2010 23:00:22 +0100 |
wenzelm |
modernized translations;
|
file |
diff |
annotate
|
| Wed, 13 Jan 2010 08:56:15 +0100 |
haftmann |
some syntax setup for Scala
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 15:32:21 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Thu, 22 Oct 2009 13:48:06 +0200 |
haftmann |
map_range (and map_index) combinator
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 16:27:32 +0200 |
haftmann |
prefer code_inline over code_unfold; use code_unfold_post where appropriate
|
file |
diff |
annotate
|
| Tue, 14 Jul 2009 10:54:04 +0200 |
haftmann |
code attributes use common underscore convention
|
file |
diff |
annotate
|
| Mon, 08 Jun 2009 08:38:52 +0200 |
haftmann |
constant "chars" of all characters
|
file |
diff |
annotate
|
| Tue, 19 May 2009 16:54:55 +0200 |
haftmann |
String.literal replaces message_string, code_numeral replaces (code_)index
|
file |
diff |
annotate
|
| Sun, 17 May 2009 07:17:39 +0200 |
haftmann |
is a definition
|
file |
diff |
annotate
|
| Sat, 16 May 2009 20:17:59 +0200 |
bulwahn |
added new kind generated_theorem for theorems which are generated by packages to distinguish between theorems from users and packages
|
file |
diff |
annotate
|
| Wed, 06 May 2009 19:09:31 +0200 |
haftmann |
proper structures for list and string code generation stuff
|
file |
diff |
annotate
|
| Wed, 06 May 2009 16:01:23 +0200 |
haftmann |
refined HOL string theories and corresponding ML fragments
|
file |
diff |
annotate
|
| Tue, 16 Jan 2001 00:30:06 +0100 |
wenzelm |
improved string syntax (allow translation rules);
|
file |
diff |
annotate
|
| Sat, 23 Dec 2000 22:50:19 +0100 |
wenzelm |
Tools/string_syntax.ML;
|
file |
diff |
annotate
|
| Mon, 16 Aug 1999 22:07:12 +0200 |
wenzelm |
'a list: Nil, Cons;
|
file |
diff |
annotate
|
| Wed, 17 Mar 1999 17:18:54 +0100 |
wenzelm |
xstr token class;
|
file |
diff |
annotate
|
| Fri, 03 Jul 1998 17:33:47 +0200 |
wenzelm |
moved String theory to main HOL;
|
file |
diff |
annotate
|