Thu, 15 Mar 2012 22:08:53 +0100 |
wenzelm |
declare command keywords via theory header, including strict checking outside Pure;
|
file |
diff |
annotate
|
Thu, 23 Feb 2012 20:15:59 +0100 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
Tue, 21 Feb 2012 08:15:42 +0100 |
haftmann |
reverting changesets from 5d33a3269029 on: change of order of declaration of classical rules makes serious problems
|
file |
diff |
annotate
|
Mon, 20 Feb 2012 21:04:00 +0100 |
haftmann |
tuned whitespace
|
file |
diff |
annotate
|
Sun, 01 Jan 2012 15:44:15 +0100 |
haftmann |
interaction of set operations for execution and membership predicate
|
file |
diff |
annotate
|
Thu, 29 Dec 2011 10:47:55 +0100 |
haftmann |
attribute code_abbrev superseedes code_unfold_post
|
file |
diff |
annotate
|
Mon, 26 Dec 2011 18:32:43 +0100 |
haftmann |
moved various set operations to theory Set (resp. Product_Type)
|
file |
diff |
annotate
|
Wed, 30 Nov 2011 18:07:14 +0100 |
wenzelm |
prefer typedef without alternative name;
|
file |
diff |
annotate
|
Wed, 30 Nov 2011 16:27:10 +0100 |
wenzelm |
prefer typedef without extra definition and alternative name;
|
file |
diff |
annotate
|
Mon, 28 Nov 2011 11:22:36 +0100 |
nipkow |
Hide Product_Type.Times - too precious an identifier
|
file |
diff |
annotate
|
Sun, 20 Nov 2011 21:07:10 +0100 |
wenzelm |
eliminated obsolete "standard";
|
file |
diff |
annotate
|
Wed, 19 Oct 2011 17:45:25 +0200 |
huffman |
merged
|
file |
diff |
annotate
|
Tue, 18 Oct 2011 15:19:06 +0200 |
huffman |
hide typedef-generated constants Product_Type.prod and Sum_Type.sum
|
file |
diff |
annotate
|
Wed, 19 Oct 2011 08:37:22 +0200 |
bulwahn |
removing old code generator setup of inductive predicates
|
file |
diff |
annotate
|
Wed, 19 Oct 2011 08:37:21 +0200 |
bulwahn |
removing old code generator setup for product types
|
file |
diff |
annotate
|
Tue, 13 Sep 2011 17:07:33 -0700 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
Mon, 08 Aug 2011 10:32:55 -0700 |
huffman |
rename Pair_fst_snd_eq to prod_eq_iff (keeping old name too)
|
file |
diff |
annotate
|
Sun, 17 Jul 2011 19:48:02 +0200 |
haftmann |
moving UNIV = ... equations to their proper theories
|
file |
diff |
annotate
|
Sat, 02 Jul 2011 22:55:58 +0200 |
haftmann |
install case certificate for If after code_datatype declaration for bool
|
file |
diff |
annotate
|
Wed, 29 Jun 2011 18:12:34 +0200 |
wenzelm |
modernized some simproc setup;
|
file |
diff |
annotate
|
Wed, 29 Jun 2011 17:35:46 +0200 |
wenzelm |
modernized some simproc setup;
|
file |
diff |
annotate
|
Tue, 19 Apr 2011 23:57:28 +0200 |
wenzelm |
eliminated Codegen.mode in favour of explicit argument;
|
file |
diff |
annotate
|
Fri, 08 Apr 2011 13:31:16 +0200 |
wenzelm |
explicit structure Syntax_Trans;
|
file |
diff |
annotate
|
Wed, 06 Apr 2011 13:33:46 +0200 |
wenzelm |
typed_print_translation: discontinued show_sorts argument;
|
file |
diff |
annotate
|
Thu, 24 Mar 2011 16:56:19 +0100 |
wenzelm |
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
|
file |
diff |
annotate
|
Tue, 22 Mar 2011 12:49:07 +0100 |
nipkow |
fixed a printing problem for bounded quantifiers and bounded set operators in the case of tuples
|
file |
diff |
annotate
|
Mon, 21 Feb 2011 10:44:19 +0100 |
blanchet |
renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
|
file |
diff |
annotate
|
Tue, 11 Jan 2011 14:12:37 +0100 |
haftmann |
"enriched_type" replaces less specific "type_lifting"
|
file |
diff |
annotate
|
Tue, 21 Dec 2010 17:52:23 +0100 |
haftmann |
tuned type_lifting declarations
|
file |
diff |
annotate
|
Fri, 17 Dec 2010 17:43:54 +0100 |
wenzelm |
replaced command 'nonterminals' by slightly modernized version 'nonterminal';
|
file |
diff |
annotate
|
Mon, 06 Dec 2010 09:19:10 +0100 |
haftmann |
replace `type_mapper` by the more adequate `type_lifting`
|
file |
diff |
annotate
|
Fri, 03 Dec 2010 10:03:13 +0100 |
huffman |
theorem names generated by the (rep_)datatype command now have mandatory qualifiers
|
file |
diff |
annotate
|
Mon, 22 Nov 2010 10:34:33 +0100 |
hoelzl |
Replace surj by abbreviation; remove surj_on.
|
file |
diff |
annotate
|
Thu, 18 Nov 2010 17:01:16 +0100 |
haftmann |
map_pair replaces prod_fun
|
file |
diff |
annotate
|
Tue, 16 Nov 2010 16:36:57 -0800 |
huffman |
typedef (open) unit
|
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:21:25 +0200 |
haftmann |
Haskell == is infix, not infixl
|
file |
diff |
annotate
|
Tue, 07 Sep 2010 10:05:19 +0200 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
Fri, 27 Aug 2010 19:34:23 +0200 |
haftmann |
renamed class/constant eq to equal; tuned some instantiations
|
file |
diff |
annotate
|
Wed, 25 Aug 2010 18:36:22 +0200 |
wenzelm |
renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
Tue, 13 Jul 2010 18:01:42 +0200 |
bulwahn |
correcting function name of generator for products of traditional code generator (introduced in 0040bafffdef)
|
file |
diff |
annotate
|
Mon, 12 Jul 2010 08:58:13 +0200 |
haftmann |
dropped superfluous [code del]s
|
file |
diff |
annotate
|
Fri, 09 Jul 2010 08:11:10 +0200 |
haftmann |
nicer xsymbol syntax for fcomp and scomp
|
file |
diff |
annotate
|
Sat, 03 Jul 2010 00:50:35 +0200 |
blanchet |
adapt Nitpick to "prod_case" and "*" -> "sum" renaming;
|
file |
diff |
annotate
|
Thu, 01 Jul 2010 16:54:44 +0200 |
haftmann |
"prod" and "sum" replace "*" and "+" respectively
|
file |
diff |
annotate
|
Mon, 28 Jun 2010 15:03:07 +0200 |
haftmann |
merged constants "split" and "prod_case"
|
file |
diff |
annotate
|
Mon, 14 Jun 2010 15:10:36 +0200 |
haftmann |
removed simplifier congruence rule of "prod_case"
|
file |
diff |
annotate
|
Thu, 10 Jun 2010 12:24:01 +0200 |
haftmann |
qualified type "*"; qualified constants Pair, fst, snd, split
|
file |
diff |
annotate
|
Tue, 08 Jun 2010 16:37:19 +0200 |
haftmann |
qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
|
file |
diff |
annotate
|
Wed, 02 Jun 2010 12:40:12 +0200 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
Fri, 28 May 2010 13:37:28 +0200 |
haftmann |
more coherent theory structure; tuned headings
|
file |
diff |
annotate
|
Wed, 26 May 2010 16:05:25 +0200 |
haftmann |
dropped legacy theorem bindings
|
file |
diff |
annotate
|
Wed, 05 May 2010 00:59:59 +0200 |
krauss |
repaired comments where SOMEthing went utterly wrong (cf. 2b04504fcb69)
|
file |
diff |
annotate
|
Tue, 20 Apr 2010 17:58:34 +0200 |
hoelzl |
Generalize swap_inj_on; add simps for Times; add Ex_list_of_length, log_inj; Added missing locale edges for linordered semiring with 1.
|
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
|
Thu, 18 Mar 2010 13:59:20 +0100 |
blanchet |
merged
|
file |
diff |
annotate
|
Thu, 18 Mar 2010 12:58:52 +0100 |
blanchet |
now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
|
file |
diff |
annotate
|
Thu, 18 Mar 2010 13:56:34 +0100 |
haftmann |
lemma swap_inj_on, swap_product
|
file |
diff |
annotate
|
Tue, 02 Mar 2010 23:59:54 +0100 |
wenzelm |
proper (type_)notation;
|
file |
diff |
annotate
|
Thu, 25 Feb 2010 22:46:52 +0100 |
wenzelm |
modernized structure Split_Rule;
|
file |
diff |
annotate
|
Thu, 25 Feb 2010 22:32:09 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Thu, 11 Feb 2010 23:00:22 +0100 |
wenzelm |
modernized translations;
|
file |
diff |
annotate
|
Thu, 14 Jan 2010 17:47:39 +0100 |
haftmann |
tuned for products vs. tupled functions
|
file |
diff |
annotate
|
Wed, 13 Jan 2010 08:56:15 +0100 |
haftmann |
some syntax setup for Scala
|
file |
diff |
annotate
|
Wed, 25 Nov 2009 11:16:57 +0100 |
haftmann |
bootstrap datatype_rep_proofs in Datatype.thy (avoids unchecked dynamic name references)
|
file |
diff |
annotate
|
Thu, 12 Nov 2009 17:21:43 +0100 |
hoelzl |
Renamed upd_snd_conv to apsnd_conv to be consistent with apfst_conv; Added apsnd_apfst_commute
|
file |
diff |
annotate
|
Tue, 10 Nov 2009 16:11:39 +0100 |
haftmann |
lemmas about apfst and apsnd
|
file |
diff |
annotate
|
Wed, 28 Oct 2009 17:44:03 +0100 |
haftmann |
load Product_Type before Nat; dropped junk
|
file |
diff |
annotate
|
Wed, 28 Oct 2009 11:42:31 +0000 |
paulson |
New theory Probability, which contains a development of measure theory
|
file |
diff |
annotate
|
Sat, 24 Oct 2009 18:55:27 +0200 |
wenzelm |
import theory Nat here, which avoids duplicate definition of datatype_realizers (and thus allows to maintain fully authentic fact table);
|
file |
diff |
annotate
|
Thu, 15 Oct 2009 23:28:10 +0200 |
wenzelm |
replaced String.concat by implode;
|
file |
diff |
annotate
|
Wed, 15 Jul 2009 23:48:21 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Tue, 23 Jun 2009 12:09:30 +0200 |
haftmann |
uniformly capitialized names for subdirectories
|
file |
diff |
annotate
|
Fri, 19 Jun 2009 17:23:21 +0200 |
haftmann |
discontinued ancient tradition to suffix certain ML module names with "_package"
|
file |
diff |
annotate
|
Tue, 16 Jun 2009 16:36:56 +0200 |
haftmann |
dropped ID
|
file |
diff |
annotate
|
Wed, 10 Jun 2009 15:04:33 +0200 |
haftmann |
separate directory for datatype package
|
file |
diff |
annotate
|
Tue, 19 May 2009 13:57:31 +0200 |
haftmann |
pretty printing of functional combinators for evaluation code
|
file |
diff |
annotate
|
Wed, 15 Apr 2009 15:30:38 +0200 |
haftmann |
default instantiation for unit type
|
file |
diff |
annotate
|
Fri, 20 Mar 2009 10:43:53 +0100 |
berghofe |
split_codegen now eta-expands terms on-the-fly.
|
file |
diff |
annotate
|
Thu, 06 Nov 2008 11:52:42 +0100 |
nipkow |
added lemma
|
file |
diff |
annotate
|
Fri, 10 Oct 2008 06:45:53 +0200 |
haftmann |
`code func` now just `code`
|
file |
diff |
annotate
|
Thu, 09 Oct 2008 08:47:27 +0200 |
haftmann |
established canonical argument order in SML code generators
|
file |
diff |
annotate
|
Thu, 25 Sep 2008 09:28:03 +0200 |
haftmann |
discontinued special treatment of op = vs. eq_class.eq
|
file |
diff |
annotate
|
Wed, 17 Sep 2008 21:27:08 +0200 |
wenzelm |
back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
|
file |
diff |
annotate
|
Tue, 10 Jun 2008 15:30:33 +0200 |
haftmann |
rep_datatype command now takes list of constructors as input arguments
|
file |
diff |
annotate
|
Fri, 23 May 2008 16:41:39 +0200 |
berghofe |
Replaced Pretty.str and Pretty.string_of by specific functions (from Codegen) that
|
file |
diff |
annotate
|
Wed, 07 May 2008 10:56:40 +0200 |
berghofe |
split_beta is now declared as monotonicity rule, to allow bounded
|
file |
diff |
annotate
|
Wed, 09 Apr 2008 08:10:11 +0200 |
haftmann |
removed syntax from monad combinators; renamed mbind to scomp
|
file |
diff |
annotate
|
Sat, 29 Mar 2008 19:14:00 +0100 |
wenzelm |
replaced 'ML_setup' by 'ML';
|
file |
diff |
annotate
|
Thu, 20 Mar 2008 12:04:54 +0100 |
haftmann |
Product_Type.apfst and Product_Type.apsnd; mbind combinator; tuned
|
file |
diff |
annotate
|
Wed, 19 Mar 2008 22:47:38 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Tue, 26 Feb 2008 11:18:43 +0100 |
bulwahn |
Added useful general lemmas from the work with the HeapMonad
|
file |
diff |
annotate
|
Thu, 10 Jan 2008 19:09:21 +0100 |
berghofe |
New interface for test data generators.
|
file |
diff |
annotate
|
Wed, 05 Dec 2007 14:15:45 +0100 |
haftmann |
simplified infrastructure for code generator operational equality
|
file |
diff |
annotate
|
Fri, 30 Nov 2007 20:13:05 +0100 |
haftmann |
more canonical attribute application
|
file |
diff |
annotate
|
Thu, 04 Oct 2007 19:54:44 +0200 |
haftmann |
certificates for code generator case expressions
|
file |
diff |
annotate
|
Tue, 25 Sep 2007 12:16:08 +0200 |
haftmann |
datatype interpretators for size and datatype_realizer
|
file |
diff |
annotate
|
Wed, 15 Aug 2007 12:52:56 +0200 |
paulson |
ATP blacklisting is now in theory data, attribute noatp
|
file |
diff |
annotate
|
Tue, 07 Aug 2007 09:38:44 +0200 |
haftmann |
split off theory Option for benefit of code generator
|
file |
diff |
annotate
|
Tue, 05 Jun 2007 15:16:08 +0200 |
haftmann |
merged Code_Generator.thy into HOL.thy
|
file |
diff |
annotate
|
Wed, 09 May 2007 07:53:06 +0200 |
haftmann |
moved recfun_codegen.ML to Code_Generator.thy
|
file |
diff |
annotate
|
Sun, 06 May 2007 21:49:23 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
Fri, 20 Apr 2007 11:21:42 +0200 |
haftmann |
Isar definitions are now added explicitly to code theorem table
|
file |
diff |
annotate
|
Wed, 04 Apr 2007 00:10:59 +0200 |
wenzelm |
ML antiquotes;
|
file |
diff |
annotate
|
Mon, 12 Mar 2007 19:23:49 +0100 |
wenzelm |
syntax: proper body priorty for derived binders;
|
file |
diff |
annotate
|
Fri, 02 Mar 2007 15:43:20 +0100 |
haftmann |
using "fst" "snd" for Haskell code
|
file |
diff |
annotate
|
Fri, 23 Feb 2007 08:39:22 +0100 |
haftmann |
slight cleanup
|
file |
diff |
annotate
|
Wed, 27 Dec 2006 19:09:57 +0100 |
haftmann |
moved code generator product setup here
|
file |
diff |
annotate
|
Wed, 22 Nov 2006 10:20:12 +0100 |
haftmann |
dropped eq const
|
file |
diff |
annotate
|
Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
Mon, 13 Nov 2006 15:43:08 +0100 |
haftmann |
added thy dependencies
|
file |
diff |
annotate
|
Tue, 07 Nov 2006 11:47:57 +0100 |
wenzelm |
renamed 'const_syntax' to 'notation';
|
file |
diff |
annotate
|
Mon, 06 Nov 2006 16:28:36 +0100 |
haftmann |
two further lemmas on split
|
file |
diff |
annotate
|
Mon, 16 Oct 2006 14:07:31 +0200 |
haftmann |
moved HOL code generator setup to Code_Generator
|
file |
diff |
annotate
|
Tue, 19 Sep 2006 15:21:42 +0200 |
haftmann |
added operational equality
|
file |
diff |
annotate
|
Fri, 25 Aug 2006 18:45:57 +0200 |
paulson |
explicit type variables prevent empty sorts
|
file |
diff |
annotate
|
Mon, 14 Aug 2006 13:46:06 +0200 |
haftmann |
simplified code generator setup
|
file |
diff |
annotate
|
Wed, 12 Jul 2006 17:00:22 +0200 |
haftmann |
adaptions in codegen
|
file |
diff |
annotate
|
Sat, 08 Jul 2006 12:54:30 +0200 |
wenzelm |
simprocs: no theory argument -- use simpset context instead;
|
file |
diff |
annotate
|
Tue, 16 May 2006 21:33:01 +0200 |
wenzelm |
tuned concrete syntax -- abbreviation/const_syntax;
|
file |
diff |
annotate
|