| Tue, 01 Jun 2010 15:38:47 +0200 |
removed "nitpick_intro" attribute -- Nitpick noew uses Spec_Rules instead
|
file | diff | annotate |
| Mon, 17 May 2010 23:54:15 +0200 |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file | diff | annotate |
| Mon, 17 May 2010 15:05:32 +0200 |
tuned;
|
file | diff | annotate |
| Sun, 16 May 2010 00:02:11 +0200 |
prefer structure Parse_Spec;
|
file | diff | annotate |
| Wed, 05 May 2010 18:25:34 +0200 |
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 |
Corrected handling of "for" parameters.
|
file | diff | annotate |
| Fri, 30 Apr 2010 18:06:29 +0200 |
proper context for rule_by_tactic;
|
file | diff | annotate |
| Wed, 28 Apr 2010 11:26:10 +0200 |
fix "fors" for proof of monotonicity
|
file | diff | annotate |
| Fri, 12 Mar 2010 12:14:31 +0100 |
adding Spec_Rules to definitional package inductive and inductive_set
|
file | diff | annotate |
| Mon, 08 Mar 2010 15:00:34 +0100 |
Added inducts field to inductive_result.
|
file | diff | annotate |
| Sun, 07 Mar 2010 12:19:47 +0100 |
modernized structure Object_Logic;
|
file | diff | annotate |
| Sun, 07 Mar 2010 11:57:16 +0100 |
modernized structure Local_Defs;
|
file | diff | annotate |
| Thu, 25 Feb 2010 22:32:09 +0100 |
more antiquotations;
|
file | diff | annotate |
| Wed, 10 Feb 2010 14:12:04 +0100 |
moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
|
file | diff | annotate |
| Sun, 31 Jan 2010 15:22:40 +0100 |
merged
|
file | diff | annotate |
| Sat, 30 Jan 2010 16:56:28 +0100 |
Added "constraints" tag / attribute for specifying the number of equality
|
file | diff | annotate |
| Thu, 28 Jan 2010 11:48:49 +0100 |
new theory Algebras.thy for generic algebraic structures
|
file | diff | annotate |
| Mon, 30 Nov 2009 08:08:31 +0100 |
merged
|
file | diff | annotate |
| Wed, 25 Nov 2009 09:13:46 +0100 |
normalized uncurry take/drop
|
file | diff | annotate |
| Tue, 24 Nov 2009 17:28:25 +0100 |
curried take/drop
|
file | diff | annotate |
| Fri, 27 Nov 2009 16:24:31 +0100 |
Simplified treatment of monotonicity rules.
|
file | diff | annotate |
| Thu, 19 Nov 2009 14:46:33 +0100 |
adapted Local_Theory.define -- eliminated odd thm kind;
|
file | diff | annotate |
| Tue, 17 Nov 2009 14:51:57 +0100 |
eliminated slightly odd name space grouping -- now managed by Isar toplevel;
|
file | diff | annotate |
| Fri, 13 Nov 2009 21:11:15 +0100 |
modernized structure Local_Theory;
|
file | diff | annotate |
| Fri, 13 Nov 2009 20:41:29 +0100 |
eliminated slightly odd kind argument of LocalTheory.note(s);
|
file | diff | annotate |
| Fri, 13 Nov 2009 19:57:46 +0100 |
inductive: eliminated obsolete kind;
|
file | diff | annotate |
| Fri, 13 Nov 2009 17:25:09 +0100 |
eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);
|
file | diff | annotate |
| Thu, 12 Nov 2009 22:02:11 +0100 |
eliminated obsolete "internal" kind -- collapsed to unspecific "";
|
file | diff | annotate |
| Tue, 10 Nov 2009 18:32:41 +0100 |
merged
|
file | diff | annotate |
| Tue, 10 Nov 2009 16:04:57 +0100 |
modernized structure Theory_Target;
|
file | diff | annotate |
| Tue, 10 Nov 2009 13:54:00 +0100 |
merged, and renamed local "TheoryData" to "Data" (following common Isabelle conventions)
|
file | diff | annotate |
| Thu, 05 Nov 2009 11:58:36 +0100 |
merged
|
file | diff | annotate |
| Thu, 05 Nov 2009 11:58:07 +0100 |
added "nitpick_def" attribute to lfp/gfp definition generated by the inductive package;
|
file | diff | annotate |
| Sun, 08 Nov 2009 16:30:41 +0100 |
adapted Generic_Data, Proof_Data;
|
file | diff | annotate |
| Thu, 05 Nov 2009 23:59:23 +0100 |
tuned;
|
file | diff | annotate |
| Thu, 05 Nov 2009 22:59:57 +0100 |
proper naming convention lthy: local_theory, but ctxt: Proof.context for arbitrary context;
|
file | diff | annotate |
| Thu, 05 Nov 2009 22:08:47 +0100 |
adapted LocalTheory.declaration;
|
file | diff | annotate |
| Sun, 01 Nov 2009 15:44:26 +0100 |
modernized structure Context_Rules;
|
file | diff | annotate |
| Sun, 01 Nov 2009 15:24:45 +0100 |
modernized structure Rule_Cases;
|
file | diff | annotate |
| Thu, 29 Oct 2009 23:49:55 +0100 |
eliminated some old folds;
|
file | diff | annotate |
| Thu, 29 Oct 2009 17:58:26 +0100 |
standardized filter/filter_out;
|
file | diff | annotate |
| Wed, 28 Oct 2009 16:25:27 +0100 |
conceal internal bindings;
|
file | diff | annotate |
| Sun, 25 Oct 2009 19:21:34 +0100 |
name space groups are identified by serial, not serial_string;
|
file | diff | annotate |
| Sat, 24 Oct 2009 19:47:37 +0200 |
renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
|
file | diff | annotate |
| Thu, 22 Oct 2009 16:52:06 +0200 |
arg_types_of auxiliary function; using multiset operations
|
file | diff | annotate |
| Wed, 21 Oct 2009 17:34:35 +0200 |
renamed "nitpick_const_xxx" attributes to "nitpick_xxx" and "nitpick_ind_intros" to "nitpick_intros"
|
file | diff | annotate |
| Wed, 21 Oct 2009 15:54:01 +0200 |
more accurate removal
|
file | diff | annotate |
| Wed, 21 Oct 2009 10:15:31 +0200 |
removed old-style \ and \\ infixes
|
file | diff | annotate |
| Sat, 17 Oct 2009 16:58:03 +0200 |
operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
|
file | diff | annotate |
| Thu, 15 Oct 2009 23:28:10 +0200 |
replaced String.concat by implode;
|
file | diff | annotate |
| Wed, 30 Sep 2009 08:22:07 +0200 |
mandatory prefix where appropriate
|
file | diff | annotate |
| Wed, 23 Sep 2009 12:03:47 +0200 |
stripped legacy ML bindings
|
file | diff | annotate |
| Fri, 18 Sep 2009 16:00:56 +0200 |
rewrite premises in tactical proof also with inf_fun_eq and inf_bool_eq: attempt to allow user to use inf [=>] and inf [bool] in his specs
|
file | diff | annotate |
| Fri, 18 Sep 2009 09:07:49 +0200 |
more antiquotations
|
file | diff | annotate |
| Fri, 24 Jul 2009 22:59:08 +0200 |
more antiquotations instead of adhoc ML stuff;
|
file | diff | annotate |
| Fri, 24 Jul 2009 18:58:58 +0200 |
renamed functor ProjectRuleFun to Project_Rule;
|
file | diff | annotate |
| Thu, 23 Jul 2009 18:44:09 +0200 |
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
|
file | diff | annotate |
| Tue, 21 Jul 2009 01:03:18 +0200 |
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
|
file | diff | annotate |
| Fri, 17 Jul 2009 23:11:40 +0200 |
tuned/modernized Envir.subst_XXX;
|
file | diff | annotate |
| Fri, 10 Jul 2009 07:59:27 +0200 |
dropped find_index_eq
|
file | diff | annotate |