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
|
Tue, 22 Jan 2013 14:33:45 +0100 |
traytel |
separate data used for case translation from the datatype package
|
file |
diff |
annotate
|
Tue, 22 Jan 2013 13:32:41 +0100 |
berghofe |
case translations performed in a separate check phase (with adjustments by traytel)
|
file |
diff |
annotate
|
Wed, 27 Mar 2013 14:19:18 +0100 |
wenzelm |
tuned signature and module arrangement;
|
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
|
Thu, 30 Aug 2012 09:47:46 +0200 |
blanchet |
more work on BNF sugar -- up to derivation of nchotomy
|
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
|
Tue, 13 Mar 2012 20:04:24 +0100 |
wenzelm |
more explicit indication of def names;
|
file |
diff |
annotate
|
Mon, 27 Feb 2012 15:48:02 +0100 |
wenzelm |
prefer cut_tac, where it is clear that the special variants cut_rules_tac or cut_facts_tac are not required;
|
file |
diff |
annotate
|
Sat, 17 Dec 2011 13:08:03 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sat, 17 Dec 2011 12:42:10 +0100 |
wenzelm |
clarified modules that contribute to datatype package;
|
file |
diff |
annotate
|
Fri, 16 Dec 2011 21:23:21 +0100 |
wenzelm |
eliminated old-fashioned Global_Theory.add_thms(s);
|
file |
diff |
annotate
|
Thu, 15 Dec 2011 18:08:40 +0100 |
wenzelm |
clarified module dependencies: Datatype_Data, Datatype_Case, Rep_Datatype;
|
file |
diff |
annotate
|
Thu, 15 Dec 2011 17:37:14 +0100 |
wenzelm |
separate rep_datatype.ML;
|
file |
diff |
annotate
|