| 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
|
| Fri, 30 Apr 2010 18:06:29 +0200 |
wenzelm |
proper context for rule_by_tactic;
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 11:26:10 +0200 |
haftmann |
fix "fors" for proof of monotonicity
|
file |
diff |
annotate
|
| Fri, 12 Mar 2010 12:14:31 +0100 |
bulwahn |
adding Spec_Rules to definitional package inductive and inductive_set
|
file |
diff |
annotate
|
| Mon, 08 Mar 2010 15:00:34 +0100 |
berghofe |
Added inducts field to inductive_result.
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 12:19:47 +0100 |
wenzelm |
modernized structure Object_Logic;
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 11:57:16 +0100 |
wenzelm |
modernized structure Local_Defs;
|
file |
diff |
annotate
|
| Thu, 25 Feb 2010 22:32:09 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Wed, 10 Feb 2010 14:12:04 +0100 |
haftmann |
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
|
file |
diff |
annotate
|
| Sun, 31 Jan 2010 15:22:40 +0100 |
berghofe |
merged
|
file |
diff |
annotate
|
| Sat, 30 Jan 2010 16:56:28 +0100 |
berghofe |
Added "constraints" tag / attribute for specifying the number of equality
|
file |
diff |
annotate
|
| Thu, 28 Jan 2010 11:48:49 +0100 |
haftmann |
new theory Algebras.thy for generic algebraic structures
|
file |
diff |
annotate
|
| Mon, 30 Nov 2009 08:08:31 +0100 |
haftmann |
merged
|
file |
diff |
annotate
|
| Wed, 25 Nov 2009 09:13:46 +0100 |
haftmann |
normalized uncurry take/drop
|
file |
diff |
annotate
|
| Tue, 24 Nov 2009 17:28:25 +0100 |
haftmann |
curried take/drop
|
file |
diff |
annotate
|
| Fri, 27 Nov 2009 16:24:31 +0100 |
berghofe |
Simplified treatment of monotonicity rules.
|
file |
diff |
annotate
|
| Thu, 19 Nov 2009 14:46:33 +0100 |
wenzelm |
adapted Local_Theory.define -- eliminated odd thm kind;
|
file |
diff |
annotate
|
| Tue, 17 Nov 2009 14:51:57 +0100 |
wenzelm |
eliminated slightly odd name space grouping -- now managed by Isar toplevel;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 21:11:15 +0100 |
wenzelm |
modernized structure Local_Theory;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 20:41:29 +0100 |
wenzelm |
eliminated slightly odd kind argument of LocalTheory.note(s);
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 19:57:46 +0100 |
wenzelm |
inductive: eliminated obsolete kind;
|
file |
diff |
annotate
|