| Sat, 27 Jul 2013 16:35:51 +0200 |
wenzelm |
standardized aliases;
|
file |
diff |
annotate
|
| Fri, 17 May 2013 20:41:45 +0200 |
wenzelm |
proper option quick_and_dirty;
|
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, 09 Apr 2013 15:29:25 +0200 |
wenzelm |
discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
|
file |
diff |
annotate
|
| Sat, 30 Mar 2013 13:40:19 +0100 |
wenzelm |
more item markup;
|
file |
diff |
annotate
|
| Fri, 29 Mar 2013 22:14:27 +0100 |
wenzelm |
Pretty.item markup for improved readability of lists of items;
|
file |
diff |
annotate
|
| Wed, 27 Mar 2013 14:19:18 +0100 |
wenzelm |
tuned signature and module arrangement;
|
file |
diff |
annotate
|
| Tue, 08 Jan 2013 16:01:07 +0100 |
wenzelm |
prefer negative "consumes", relative to the total number of prems, which is stable under more morphisms, notably those from nested context with assumes (cf. existing treatment of 'obtains');
|
file |
diff |
annotate
|
| Fri, 30 Nov 2012 22:55:02 +0100 |
wenzelm |
added 'print_inductives' command;
|
file |
diff |
annotate
|
| Fri, 30 Nov 2012 22:38:06 +0100 |
wenzelm |
print formal entities with markup;
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 14:43:28 +0100 |
wenzelm |
tuned command descriptions;
|
file |
diff |
annotate
|
| Wed, 12 Sep 2012 14:46:13 +0200 |
wenzelm |
removed obsolete argument "int" and thus made SML/NJ happy (cf. 03bee3a6a1b7);
|
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, 10 May 2012 20:49:30 +0200 |
wenzelm |
tweaked Inductive.prove_eqs to allow degenerate definition like "inductive TRUE where TRUE";
|
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
|
| Thu, 15 Mar 2012 20:07:00 +0100 |
wenzelm |
prefer formally checked @{keyword} parser;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 19:02:34 +0100 |
wenzelm |
declare minor keywords via theory header;
|
file |
diff |
annotate
|
| Wed, 14 Mar 2012 11:10:10 +0100 |
wenzelm |
more parallel inductive_cases;
|
file |
diff |
annotate
|
| Mon, 12 Mar 2012 23:33:50 +0100 |
wenzelm |
some grouping of Par_List operations, to adjust granularity;
|
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, 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
|
| Fri, 02 Dec 2011 14:54:25 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Sun, 27 Nov 2011 22:20:07 +0100 |
wenzelm |
permissive update for improved "tool compliance";
|
file |
diff |
annotate
|
| Sun, 27 Nov 2011 22:03:22 +0100 |
wenzelm |
just one data slot per module;
|
file |
diff |
annotate
|
| Sun, 27 Nov 2011 14:40:08 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 27 Nov 2011 14:26:57 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Sun, 27 Nov 2011 14:20:31 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Sat, 19 Nov 2011 21:18:38 +0100 |
wenzelm |
added ML antiquotation @{attributes};
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 22:17:30 +0200 |
wenzelm |
uniform Local_Theory.declaration with explicit params;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2011 17:15:52 +0200 |
wenzelm |
tuned signature -- refined terminology;
|
file |
diff |
annotate
|
| Sat, 10 Sep 2011 19:44:41 +0200 |
haftmann |
more modularization
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 20:19:05 +0200 |
wenzelm |
more precise position information via Variable.add_fixes_binding;
|
file |
diff |
annotate
|
| Wed, 20 Apr 2011 22:57:29 +0200 |
wenzelm |
eliminated Display.string_of_thm_without_context;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 21:42:47 +0200 |
wenzelm |
added Binding.print convenience, which includes quote already;
|
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
|
| Sat, 16 Apr 2011 13:48:45 +0200 |
wenzelm |
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
|
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
|
| Fri, 17 Dec 2010 17:08:56 +0100 |
wenzelm |
renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
|
file |
diff |
annotate
|
| Wed, 08 Dec 2010 13:34:50 +0100 |
haftmann |
primitive definitions of bot/top/inf/sup for bool and fun are named with canonical suffix `_def` rather than `_eq`
|
file |
diff |
annotate
|
| Fri, 03 Dec 2010 08:40:47 +0100 |
bulwahn |
tuned
|
file |
diff |
annotate
|
| Wed, 03 Nov 2010 11:06:22 +0100 |
wenzelm |
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
|
file |
diff |
annotate
|
| Thu, 09 Sep 2010 09:11:13 +0200 |
haftmann |
only conceal primitive definition theorems, not predicate names
|
file |
diff |
annotate
|
| Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
| Mon, 23 Aug 2010 16:47:57 +0200 |
bulwahn |
introducing simplification equations for inductive sets; added data structure for storing equations; rewriting retrieval of simplification equation for inductive predicates and sets
|
file |
diff |
annotate
|
| Thu, 12 Aug 2010 13:23:46 +0200 |
haftmann |
Named_Target.theory_init
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 14:45:38 +0200 |
haftmann |
renamed Theory_Target to the more appropriate Named_Target
|
file |
diff |
annotate
|
| Sun, 01 Aug 2010 10:15:43 +0200 |
bulwahn |
inductive_simps learns to have more tool compliance
|
file |
diff |
annotate
|
| Mon, 26 Jul 2010 17:59:26 +0200 |
wenzelm |
inductive_cases: crude parallelization via Par_List.map;
|
file |
diff |
annotate
|
| Wed, 21 Jul 2010 17:57:16 +0200 |
wenzelm |
make SML/NJ happy, by adhoc type-constraints;
|
file |
diff |
annotate
|
| Wed, 07 Jul 2010 08:25:21 +0200 |
bulwahn |
added the new command inductive_cases to derive simplification equations for inductive predicates; added binding simps for general simplification equation
|
file |
diff |
annotate
|
| Tue, 01 Jun 2010 15:38:47 +0200 |
blanchet |
removed "nitpick_intro" attribute -- Nitpick noew uses Spec_Rules instead
|
file |
diff |
annotate
|
| Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
| Mon, 17 May 2010 15:05:32 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 16 May 2010 00:02:11 +0200 |
wenzelm |
prefer structure Parse_Spec;
|
file |
diff |
annotate
|
| Wed, 05 May 2010 18:25:34 +0200 |
haftmann |
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
|
file |
diff |
annotate
|
| Tue, 04 May 2010 12:29:22 +0200 |
berghofe |
Corrected handling of "for" parameters.
|
file |
diff |
annotate
|