| Sat, 27 Nov 2010 12:55:12 -0800 |
huffman |
rename cpodef theorems: lub_foo -> is_lub_foo, thelub_foo -> lub_foo
|
file |
diff |
annotate
|
| Wed, 27 Oct 2010 13:54:18 -0700 |
huffman |
rename lemmas *_defined_iff and *_strict_iff to *_bottom_iff
|
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
|
| Thu, 26 Aug 2010 13:09:12 +0200 |
wenzelm |
renamed ProofContext.theory(_result) to ProofContext.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 14:31:43 +0200 |
haftmann |
moved instantiation target formally to class_target.ML
|
file |
diff |
annotate
|
| Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
| Mon, 03 May 2010 14:25:56 +0200 |
wenzelm |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
| Sun, 25 Apr 2010 15:52:03 +0200 |
wenzelm |
modernized naming conventions of main Isar proof elements;
|
file |
diff |
annotate
|
| Tue, 20 Apr 2010 13:44:28 -0700 |
huffman |
replace many uses of Drule.export_without_context with Drule.zero_var_indexes
|
file |
diff |
annotate
|
| Thu, 15 Apr 2010 18:09:22 +0200 |
wenzelm |
replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions B.foo = A.foo;
|
file |
diff |
annotate
|
| Sat, 27 Mar 2010 21:38:38 +0100 |
wenzelm |
Typedef.info: separate global and local part, only the latter is transformed by morphisms;
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 15:53:25 -0700 |
huffman |
error -> raise Fail
|
file |
diff |
annotate
|
| Mon, 22 Mar 2010 14:11:13 -0700 |
huffman |
fix ML warnings in pcpodef.ML
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 00:43:49 +0100 |
wenzelm |
allow sort constraints in HOL/typedef and related HOLCF variants;
|
file |
diff |
annotate
|
| Sat, 13 Mar 2010 14:43:04 +0100 |
wenzelm |
global typedef;
|
file |
diff |
annotate
|
| Wed, 24 Feb 2010 20:37:01 +0100 |
wenzelm |
allow general mixfix syntax for type constructors;
|
file |
diff |
annotate
|
| Thu, 18 Feb 2010 23:37:43 +0100 |
wenzelm |
Sign.restore_naming -- slightly more robust;
|
file |
diff |
annotate
|
| Mon, 15 Feb 2010 17:17:51 +0100 |
wenzelm |
discontinued unnamed infix syntax;
|
file |
diff |
annotate
|
| Sun, 07 Feb 2010 19:33:34 +0100 |
wenzelm |
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 15:40:06 -0800 |
huffman |
merged
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 15:29:48 -0800 |
huffman |
cleaned up, removed unneeded call to Syntax.check_term
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 21:11:15 +0100 |
wenzelm |
modernized structure Local_Theory;
|
file |
diff |
annotate
|
| Thu, 12 Nov 2009 14:31:11 -0800 |
huffman |
improved ML interface to pcpodef
|
file |
diff |
annotate
|
| Wed, 11 Nov 2009 10:15:32 -0800 |
huffman |
use Drule.standard (following typedef package), add pcpodef tactic interface
|
file |
diff |
annotate
|
| Tue, 10 Nov 2009 16:04:57 +0100 |
wenzelm |
modernized structure Theory_Target;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2009 15:02:31 +0100 |
wenzelm |
comment;
|
file |
diff |
annotate
|
| Sun, 21 Jun 2009 15:45:57 +0200 |
haftmann |
discontinued ancient tradition to suffix certain ML module names with "_package"
|
file |
diff |
annotate
| base
|