2012-08-22 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
2012-03-15 |
wenzelm |
declare command keywords via theory header, including strict checking outside Pure;
|
file |
diff |
annotate
|
2012-03-15 |
wenzelm |
declare minor keywords via theory header;
|
file |
diff |
annotate
|
2011-02-08 |
wenzelm |
discontinued obsolete alias HOL.thy for @{theory HOL} in ML;
|
file |
diff |
annotate
|
2010-08-17 |
haftmann |
dropped SML typedef_codegen: does not fit to code equations for record operations any longer
|
file |
diff |
annotate
|
2010-08-12 |
haftmann |
group record-related ML files
|
file |
diff |
annotate
|
2010-07-20 |
wenzelm |
discontinued pervasive val theory = Thy_Info.get_theory -- prefer antiquotations in most situations;
|
file |
diff |
annotate
|
2009-06-19 |
haftmann |
discontinued ancient tradition to suffix certain ML module names with "_package"
|
file |
diff |
annotate
|
2009-02-03 |
haftmann |
handling type classes without parameters
|
file |
diff |
annotate
|
2009-01-21 |
haftmann |
no base sort in class import
|
file |
diff |
annotate
|
2008-12-10 |
wenzelm |
misc tuning and modernisation;
|
file |
diff |
annotate
|
2008-12-04 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
2008-09-29 |
wenzelm |
LocalTheory.exit_global;
|
file |
diff |
annotate
|
2008-09-02 |
wenzelm |
type Attrib.binding abbreviates Name.binding without attributes;
|
file |
diff |
annotate
|
2008-09-02 |
wenzelm |
explicit type Name.binding for higher-specification elements;
|
file |
diff |
annotate
|
2008-06-20 |
huffman |
add lemma Abs_image
|
file |
diff |
annotate
|
2008-05-07 |
berghofe |
Deleted instantiation "set :: (type) itself".
|
file |
diff |
annotate
|
2008-02-26 |
haftmann |
class itself works around a problem with class interpretation in class finite
|
file |
diff |
annotate
|
2007-12-05 |
haftmann |
interpretation of typedefs
|
file |
diff |
annotate
|
2007-08-14 |
huffman |
remove redundant assumption from Rep_range lemma
|
file |
diff |
annotate
|
2007-07-10 |
haftmann |
removed proof dependency on transitivity theorems
|
file |
diff |
annotate
|
2007-06-20 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
2007-06-05 |
haftmann |
merged Code_Generator.thy into HOL.thy
|
file |
diff |
annotate
|
2007-05-06 |
wenzelm |
simplified DataFun interfaces;
|
file |
diff |
annotate
|
2006-08-29 |
haftmann |
added typecopy_package
|
file |
diff |
annotate
|
2006-04-24 |
haftmann |
seperated typedef codegen from main code
|
file |
diff |
annotate
|
2005-06-17 |
haftmann |
migrated theory headers to new format
|
file |
diff |
annotate
|
2004-10-26 |
berghofe |
Added setup for code generator.
|
file |
diff |
annotate
|
2004-08-18 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
2004-08-16 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
2002-07-24 |
wenzelm |
simplified locale predicates;
|
file |
diff |
annotate
|
2002-07-23 |
wenzelm |
predicate defs via locales;
|
file |
diff |
annotate
|
2001-11-03 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2001-10-30 |
wenzelm |
lemma Least_mono moved from Typedef.thy to Set.thy;
|
file |
diff |
annotate
|
2001-10-28 |
wenzelm |
converted theory "Set";
|
file |
diff |
annotate
|
2001-10-14 |
wenzelm |
moved rulify to ObjectLogic;
|
file |
diff |
annotate
|
2001-10-13 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2001-10-03 |
wenzelm |
Tools/induct_attrib.ML now part of Pure;
|
file |
diff |
annotate
|
2001-10-03 |
wenzelm |
moved linorder_cases to theory Ord;
|
file |
diff |
annotate
|
2001-09-27 |
wenzelm |
renamed theory "subset" to "Typedef";
|
file |
diff |
annotate
|