Sun, 09 Nov 2014 20:41:53 +0100 |
wenzelm |
proper proof context for typedef;
|
file |
diff |
annotate
|
Sun, 09 Nov 2014 14:08:00 +0100 |
wenzelm |
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
|
file |
diff |
annotate
|
Thu, 18 Sep 2014 16:47:40 +0200 |
blanchet |
moved 'old_datatype' out of 'Main' (but put it in 'HOL-Proofs' because of the inductive realizer)
|
file |
diff |
annotate
|
Wed, 17 Sep 2014 08:23:53 +0200 |
blanchet |
support (finite values of) codatatypes in Quickcheck
|
file |
diff |
annotate
|
Thu, 11 Sep 2014 18:54:36 +0200 |
blanchet |
speed up old Nominal by killing type variables
|
file |
diff |
annotate
|
Mon, 08 Sep 2014 23:04:18 +0200 |
blanchet |
added flag to 'typedef' to allow concealed definitions
|
file |
diff |
annotate
|
Mon, 08 Sep 2014 23:04:18 +0200 |
blanchet |
ported old Nominal to use new datatypes
|
file |
diff |
annotate
|
Mon, 08 Sep 2014 14:03:57 +0200 |
blanchet |
use compatibility layer
|
file |
diff |
annotate
|
Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place
|
file |
diff |
annotate
|
Mon, 01 Sep 2014 16:17:46 +0200 |
blanchet |
tuned structure inclusion
|
file |
diff |
annotate
|
Sat, 22 Mar 2014 18:16:54 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Fri, 21 Mar 2014 10:45:03 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Fri, 07 Mar 2014 22:30:58 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Wed, 01 Jan 2014 14:29:22 +0100 |
wenzelm |
clarified simplifier context;
|
file |
diff |
annotate
|
Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
Tue, 30 Jul 2013 15:09:25 +0200 |
wenzelm |
type theory is purely value-oriented;
|
file |
diff |
annotate
|
Sat, 27 Apr 2013 20:50:20 +0200 |
wenzelm |
uniform Proof.context for hyp_subst_tac;
|
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
|
Wed, 10 Apr 2013 15:30:19 +0200 |
wenzelm |
more standard module name Axclass (according to file name);
|
file |
diff |
annotate
|
Wed, 10 Apr 2013 13:10:38 +0200 |
wenzelm |
formal proof context for axclass proofs;
|
file |
diff |
annotate
|
Thu, 14 Feb 2013 16:36:21 +0100 |
wenzelm |
more parallel proofs in 'nominal_datatype', although sequential dark matter remains;
|
file |
diff |
annotate
|
Fri, 12 Oct 2012 21:22:35 +0200 |
wenzelm |
discontinued typedef with alternative name;
|
file |
diff |
annotate
|
Fri, 12 Oct 2012 15:08:29 +0200 |
wenzelm |
discontinued typedef with implicit set_def;
|
file |
diff |
annotate
|
Wed, 05 Sep 2012 19:51:00 +0200 |
wenzelm |
discontinued obsolete fork_mono to loosen some brakes -- NB: TTY interaction has Goal.future_proofs disabled due to missing Future.worker_task;
|
file |
diff |
annotate
|
Fri, 16 Mar 2012 18:20:12 +0100 |
wenzelm |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
file |
diff |
annotate
|
Sat, 14 Jan 2012 21:16:15 +0100 |
wenzelm |
discontinued old-style Term.list_abs in favour of plain Term.abs;
|
file |
diff |
annotate
|
Sat, 14 Jan 2012 20:05:58 +0100 |
wenzelm |
renamed Term.list_all to Logic.list_all, in accordance to HOLogic.list_all;
|
file |
diff |
annotate
|
Sat, 14 Jan 2012 17:45:04 +0100 |
wenzelm |
discontinued old-style Term.list_all_free in favour of plain Logic.all;
|
file |
diff |
annotate
|
Mon, 09 Jan 2012 18:29:42 +0100 |
wenzelm |
prefer antiquotations;
|
file |
diff |
annotate
|
Sat, 17 Dec 2011 13:08:03 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sat, 17 Dec 2011 12:10:37 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Fri, 16 Dec 2011 10:38:38 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Thu, 15 Dec 2011 17:37:14 +0100 |
wenzelm |
separate rep_datatype.ML;
|
file |
diff |
annotate
|
Thu, 15 Dec 2011 14:11:57 +0100 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
Wed, 14 Dec 2011 21:54:32 +0100 |
wenzelm |
avoid fragile Sign.intern_const -- pass internal names directly;
|
file |
diff |
annotate
|
Wed, 14 Dec 2011 15:30:17 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Tue, 13 Dec 2011 23:23:51 +0100 |
wenzelm |
'datatype' specifications allow explicit sort constraints;
|
file |
diff |
annotate
|
Tue, 13 Dec 2011 20:29:59 +0100 |
wenzelm |
do not open ML structures;
|
file |
diff |
annotate
|
Mon, 12 Dec 2011 23:05:21 +0100 |
wenzelm |
datatype dtyp with explicit sort information;
|
file |
diff |
annotate
|
Fri, 02 Dec 2011 15:23:27 +0100 |
wenzelm |
eliminated some legacy operations;
|
file |
diff |
annotate
|
Fri, 02 Dec 2011 14:54:25 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Fri, 02 Dec 2011 13:38:24 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 30 Nov 2011 23:30:08 +0100 |
wenzelm |
discontinued obsolete datatype "alt_names";
|
file |
diff |
annotate
|
Sun, 27 Nov 2011 23:10:19 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Sat, 03 Sep 2011 15:09:51 -0700 |
huffman |
merged
|
file |
diff |
annotate
|
Sat, 03 Sep 2011 14:52:40 -0700 |
huffman |
modify nominal packages to better respect set/pred distinction
|
file |
diff |
annotate
|
Sat, 03 Sep 2011 17:32:35 +0200 |
haftmann |
assert Pure equations for theorem references; avoid dynamic reference to fact
|
file |
diff |
annotate
|
Wed, 17 Aug 2011 18:05:31 +0200 |
wenzelm |
modernized signature of Term.absfree/absdummy;
|
file |
diff |
annotate
|
Wed, 10 Aug 2011 20:53:43 +0200 |
wenzelm |
old term operations are legacy;
|
file |
diff |
annotate
|
Thu, 09 Jun 2011 16:34:49 +0200 |
wenzelm |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
file |
diff |
annotate
|
Mon, 18 Apr 2011 13:52:23 +0200 |
wenzelm |
standardized aliases of operations on tsig;
|
file |
diff |
annotate
|
Sun, 17 Apr 2011 19:54:04 +0200 |
wenzelm |
report Name_Space.declare/define, relatively to context;
|
file |
diff |
annotate
|
Sat, 16 Apr 2011 18:11:20 +0200 |
wenzelm |
eliminated old List.nth;
|
file |
diff |
annotate
|
Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
Mon, 10 Jan 2011 15:19:48 +0100 |
wenzelm |
standardized split_last/last_elem towards List.last;
|
file |
diff |
annotate
|
Wed, 01 Dec 2010 15:03:44 +0100 |
wenzelm |
more direct use of binder_types/body_type;
|
file |
diff |
annotate
|
Sat, 20 Nov 2010 00:53:26 +0100 |
wenzelm |
renamed raw "explode" function to "raw_explode" to emphasize its meaning;
|
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, 06 Sep 2010 19:13:10 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|