Fri, 23 Feb 2018 19:25:37 +0100 |
wenzelm |
added HOLogic.mk_obj_eq convenience and eliminated some clones;
|
file |
diff |
annotate
|
Tue, 02 Jan 2018 14:42:00 +0100 |
blanchet |
store high-level 'size' equations
|
file |
diff |
annotate
|
Thu, 24 Aug 2017 10:47:56 +0200 |
blanchet |
tuning (proofs and code)
|
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
|
Tue, 29 Nov 2016 08:32:46 +0100 |
blanchet |
don't generate 'size_gen_o_map' property if its type variable is too limited anyway to be useful
|
file |
diff |
annotate
|
Mon, 12 Sep 2016 23:17:55 +0200 |
blanchet |
make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions
|
file |
diff |
annotate
|
Mon, 06 Jun 2016 21:28:46 +0200 |
haftmann |
explicit tagging of code equations de-baroquifies interface
|
file |
diff |
annotate
|
Thu, 02 Jun 2016 16:49:44 +0200 |
wenzelm |
eliminated pointless alias (no warning for duplicates);
|
file |
diff |
annotate
|
Fri, 27 May 2016 20:23:55 +0200 |
wenzelm |
tuned proofs, to allow unfold_abs_def;
|
file |
diff |
annotate
|
Tue, 22 Mar 2016 08:00:33 +0100 |
blanchet |
nicer error
|
file |
diff |
annotate
|
Mon, 07 Mar 2016 23:20:11 +0100 |
blanchet |
made 'size' plugin compatible with locales again (and added regression test)
|
file |
diff |
annotate
|
Mon, 11 Jan 2016 13:15:14 +0100 |
blanchet |
exported ML function
|
file |
diff |
annotate
|
Thu, 07 Jan 2016 15:53:39 +0100 |
wenzelm |
more uniform treatment of package internals;
|
file |
diff |
annotate
|
Wed, 06 Jan 2016 13:04:31 +0100 |
blanchet |
nicer 'Spec_Rules' for size function
|
file |
diff |
annotate
|
Fri, 04 Dec 2015 21:21:35 +0100 |
blanchet |
nicer error when the given size function has the wrong type
|
file |
diff |
annotate
|
Tue, 01 Dec 2015 13:07:40 +0100 |
blanchet |
tuned whitespace
|
file |
diff |
annotate
|
Tue, 06 Oct 2015 12:01:07 +0200 |
traytel |
collect the names from goals in favor of fragile exports
|
file |
diff |
annotate
|
Thu, 03 Sep 2015 16:41:43 +0200 |
traytel |
use open/close_target rather than Local_Theory.restore to get polymorphic definitions;
|
file |
diff |
annotate
|
Sun, 26 Jul 2015 17:24:54 +0200 |
wenzelm |
updated to infer_instantiate;
|
file |
diff |
annotate
|
Thu, 16 Jul 2015 12:23:22 +0200 |
traytel |
{r,e,d,f}tac with proper context in BNF
|
file |
diff |
annotate
|
Thu, 09 Apr 2015 18:00:59 +0200 |
blanchet |
fixed typo in function name
|
file |
diff |
annotate
|
Tue, 31 Mar 2015 00:11:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sat, 07 Mar 2015 00:45:15 +0100 |
wenzelm |
tuned;
|
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
|
Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
Tue, 03 Mar 2015 19:08:04 +0100 |
traytel |
eliminated some clones of Proof_Context.cterm_of
|
file |
diff |
annotate
|
Tue, 03 Mar 2015 16:37:45 +0100 |
blanchet |
strengthened 'size' tactic for examples like datatype (dead 'a, 'b) y = Y "'a * 'b"
|
file |
diff |
annotate
|
Tue, 03 Mar 2015 16:37:45 +0100 |
blanchet |
avoid duplicate simp warning for datatypes with explicit products
|
file |
diff |
annotate
|
Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
Wed, 17 Dec 2014 16:51:29 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
Fri, 07 Nov 2014 11:28:37 +0100 |
traytel |
more complete fp_sugars for sum and prod;
|
file |
diff |
annotate
|
Fri, 07 Nov 2014 11:52:54 +0100 |
desharna |
generate 'size_neq' for datatypes
|
file |
diff |
annotate
|
Tue, 21 Oct 2014 17:23:14 +0200 |
desharna |
rename 'size_o_map' to 'size_gen_o_map'
|
file |
diff |
annotate
|
Tue, 21 Oct 2014 17:23:13 +0200 |
desharna |
generate 'size_gen' for datatypes
|
file |
diff |
annotate
|
Tue, 21 Oct 2014 17:23:12 +0200 |
desharna |
generate 'map_o_corec' for (co)datatypes
|
file |
diff |
annotate
|
Tue, 21 Oct 2014 17:23:11 +0200 |
desharna |
move theorem 'rec_o_map'
|
file |
diff |
annotate
|
Mon, 13 Oct 2014 18:45:48 +0200 |
wenzelm |
Local_Interpretation is superseded by Plugin with formal Plugin_Name management, avoiding undeclared strings;
|
file |
diff |
annotate
|
Wed, 08 Oct 2014 17:09:07 +0200 |
wenzelm |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
file |
diff |
annotate
|
Mon, 06 Oct 2014 13:37:38 +0200 |
desharna |
rename 'xtor_co_rec_o_map_thms' to 'xtor_co_rec_o_maps'
|
file |
diff |
annotate
|
Fri, 26 Sep 2014 14:43:26 +0200 |
desharna |
refactor fp_sugar move theorems
|
file |
diff |
annotate
|
Fri, 26 Sep 2014 14:41:15 +0200 |
desharna |
refactor fp_sugar move theorems
|
file |
diff |
annotate
|
Thu, 18 Sep 2014 16:47:40 +0200 |
blanchet |
moved old 'size' generator together with 'old_datatype'
|
file |
diff |
annotate
|
Wed, 17 Sep 2014 08:24:10 +0200 |
blanchet |
syntactic check to determine when to prove 'nested_size_o_map'
|
file |
diff |
annotate
|
Tue, 16 Sep 2014 19:23:37 +0200 |
blanchet |
tuned fact visibility
|
file |
diff |
annotate
|
Mon, 15 Sep 2014 11:37:55 +0200 |
blanchet |
tuned definition of 'size' function to get nicer properties
|
file |
diff |
annotate
|
Mon, 15 Sep 2014 11:17:44 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Mon, 15 Sep 2014 10:49:07 +0200 |
blanchet |
generate 'code' attribute only if 'code' plugin is enabled
|
file |
diff |
annotate
|
Thu, 11 Sep 2014 19:45:42 +0200 |
blanchet |
tuning terminology
|
file |
diff |
annotate
|
Mon, 08 Sep 2014 14:03:01 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
pretend code generation is a ctr_sugar plugin
|
file |
diff |
annotate
|
Fri, 05 Sep 2014 00:41:01 +0200 |
blanchet |
named interpretations
|
file |
diff |
annotate
|
Thu, 04 Sep 2014 09:02:43 +0200 |
blanchet |
renamed internal constant
|
file |
diff |
annotate
|
Thu, 04 Sep 2014 09:02:43 +0200 |
blanchet |
moved code around
|
file |
diff |
annotate
|
Thu, 04 Sep 2014 09:02:43 +0200 |
blanchet |
tuned size function generation
|
file |
diff |
annotate
|
Mon, 01 Sep 2014 16:34:40 +0200 |
blanchet |
renamed BNF theories
|
file |
diff |
annotate
|
Tue, 19 Aug 2014 09:34:57 +0200 |
blanchet |
robustified tactics
|
file |
diff |
annotate
|
Mon, 11 Aug 2014 10:43:03 +0200 |
traytel |
use Goal.prove_sorry instead of Goal.prove where possible (= no schematics in goal and tactic is expected to succeed)
|
file |
diff |
annotate
|
Thu, 24 Jul 2014 00:24:00 +0200 |
blanchet |
use the noted theorem whenever possible, also in 'BNF_Def'
|
file |
diff |
annotate
|
Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|