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
|
Sat, 28 Aug 2010 16:14:32 +0200 |
haftmann |
formerly unnamed infix equality now named HOL.eq
|
file |
diff |
annotate
|
Fri, 27 Aug 2010 19:34:23 +0200 |
haftmann |
renamed class/constant eq to equal; tuned some instantiations
|
file |
diff |
annotate
|
Wed, 18 Aug 2010 15:01:57 +0200 |
haftmann |
liberal instantiation of class eq; tuned naming scheme
|
file |
diff |
annotate
|
Wed, 11 Aug 2010 14:31:43 +0200 |
haftmann |
moved instantiation target formally to class_target.ML
|
file |
diff |
annotate
|
Mon, 14 Jun 2010 12:01:30 +0200 |
haftmann |
explicitly name and note equations for class eq
|
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
|
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
|
Thu, 22 Apr 2010 12:07:00 +0200 |
haftmann |
swapped generic code generator and SML code generator
|
file |
diff |
annotate
|
Mon, 22 Mar 2010 20:59:22 +0100 |
wenzelm |
explicit Simplifier.global_context;
|
file |
diff |
annotate
|
Sat, 20 Mar 2010 17:33:11 +0100 |
wenzelm |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
file |
diff |
annotate
|
Mon, 30 Nov 2009 11:42:49 +0100 |
haftmann |
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
|
file |
diff |
annotate
|
Fri, 27 Nov 2009 08:42:34 +0100 |
haftmann |
renamed former datatype.ML to datatype_data.ML
|
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
|
Tue, 10 Nov 2009 16:04:57 +0100 |
wenzelm |
modernized structure Theory_Target;
|
file |
diff |
annotate
|
Thu, 29 Oct 2009 17:58:26 +0100 |
wenzelm |
standardized filter/filter_out;
|
file |
diff |
annotate
|
Wed, 21 Oct 2009 00:36:12 +0200 |
wenzelm |
standardized basic operations on type option;
|
file |
diff |
annotate
|
Tue, 20 Oct 2009 10:46:42 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
Tue, 20 Oct 2009 08:10:31 +0200 |
haftmann |
more accurate checkpoints
|
file |
diff |
annotate
|
Mon, 19 Oct 2009 16:34:12 +0200 |
haftmann |
dropped lazy code equations
|
file |
diff |
annotate
|
Mon, 19 Oct 2009 21:54:57 +0200 |
wenzelm |
uniform use of Integer.add/mult/sum/prod;
|
file |
diff |
annotate
|
Sat, 17 Oct 2009 16:58:03 +0200 |
wenzelm |
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 |
wenzelm |
replaced String.concat by implode;
|
file |
diff |
annotate
|
Mon, 12 Oct 2009 09:25:26 +0200 |
haftmann |
using distinct rules directly
|
file |
diff |
annotate
|
Thu, 08 Oct 2009 19:33:03 +0200 |
haftmann |
lookup for datatype constructors considers type annotations to resolve overloading
|
file |
diff |
annotate
|
Tue, 23 Jun 2009 16:27:12 +0200 |
haftmann |
tuned interfaces of datatype module
|
file |
diff |
annotate
|
Tue, 23 Jun 2009 12:09:30 +0200 |
haftmann |
uniformly capitialized names for subdirectories
|
file |
diff |
annotate
| base
|