| Fri, 03 Jul 2009 16:51:08 +0200 |
haftmann |
nominal.ML is nominal_datatype.ML
|
file |
diff |
annotate
|
| Mon, 29 Jun 2009 12:18:55 +0200 |
haftmann |
renamed theory Code_Set to Fset
|
file |
diff |
annotate
|
| Thu, 25 Jun 2009 17:07:18 +0200 |
haftmann |
added List_Set and Code_Set theories
|
file |
diff |
annotate
|
| Wed, 24 Jun 2009 21:46:54 +0200 |
wenzelm |
standard naming conventions for session and theories;
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 12:08:33 +0200 |
haftmann |
NewNumberTheory depends on Algebra
|
file |
diff |
annotate
|
| Tue, 23 Jun 2009 10:22:11 +0200 |
chaieb |
Added Library/Fraction_Field.thy: The fraction field of any integral
|
file |
diff |
annotate
|
| Mon, 22 Jun 2009 23:48:24 +0200 |
wenzelm |
observe standard theory naming conventions;
|
file |
diff |
annotate
|
| Sun, 21 Jun 2009 15:47:41 +0200 |
nipkow |
fixed NewNumberTheory deps
|
file |
diff |
annotate
|
| Fri, 19 Jun 2009 21:08:07 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Fri, 19 Jun 2009 17:23:21 +0200 |
haftmann |
discontinued ancient tradition to suffix certain ML module names with "_package"
|
file |
diff |
annotate
|
| Fri, 19 Jun 2009 18:33:10 +0200 |
nipkow |
Added NewNumberTheory by Jeremy Avigad
|
file |
diff |
annotate
|
| Wed, 17 Jun 2009 16:55:01 -0700 |
huffman |
new GCD library, courtesy of Jeremy Avigad
|
file |
diff |
annotate
|
| Wed, 10 Jun 2009 15:04:33 +0200 |
haftmann |
separate directory for datatype package
|
file |
diff |
annotate
|
| Tue, 09 Jun 2009 22:59:54 +0200 |
haftmann |
first running version of qc generators for datatypes
|
file |
diff |
annotate
|
| Thu, 04 Jun 2009 16:55:20 +0200 |
haftmann |
added trees implementing mappings
|
file |
diff |
annotate
|
| Tue, 02 Jun 2009 15:53:07 +0200 |
haftmann |
tuned code generator test theories
|
file |
diff |
annotate
|
| Tue, 02 Jun 2009 10:04:03 +0200 |
berghofe |
merged
|
file |
diff |
annotate
|
| Tue, 02 Jun 2009 10:00:29 +0200 |
berghofe |
Added Convex_Euclidean_Space.thy again.
|
file |
diff |
annotate
|
| Mon, 01 Jun 2009 07:45:49 -0700 |
huffman |
add dependency on Limits.thy
|
file |
diff |
annotate
|
| Thu, 28 May 2009 18:59:51 +0200 |
himmelma |
Removed Convex_Euclidean_Space.thy from Library.
|
file |
diff |
annotate
|
| Thu, 28 May 2009 13:56:50 +0200 |
himmelma |
Added Convex_Euclidean_Space to Library.thy and Library/IsaMakefile
|
file |
diff |
annotate
|
| Tue, 26 May 2009 17:29:32 +0200 |
haftmann |
separate module for quickcheck generators
|
file |
diff |
annotate
|
| Tue, 19 May 2009 16:54:55 +0200 |
haftmann |
String.literal replaces message_string, code_numeral replaces (code_)index
|
file |
diff |
annotate
|
| Tue, 19 May 2009 13:57:32 +0200 |
haftmann |
moved Code_Index, Random and Quickcheck before Main
|
file |
diff |
annotate
|
| Sat, 16 May 2009 20:16:49 +0200 |
haftmann |
experimental move of Quickcheck and related theories to HOL image
|
file |
diff |
annotate
|
| Fri, 15 May 2009 16:52:28 +0200 |
haftmann |
experimental addition of quickcheck
|
file |
diff |
annotate
|
| Fri, 15 May 2009 16:39:17 +0200 |
haftmann |
dropped theory Term_Of_Syntax
|
file |
diff |
annotate
|
| Tue, 12 May 2009 21:17:47 +0200 |
haftmann |
split Predicate_Compile examples into separate theory
|
file |
diff |
annotate
|
| Tue, 12 May 2009 20:07:05 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
| Tue, 12 May 2009 19:30:33 +0200 |
haftmann |
transferred code generator preprocessor into separate module
|
file |
diff |
annotate
|