| 2006-11-06 |
haftmann |
code generator module naming improved
|
file |
diff |
annotate
|
| 2006-10-16 |
haftmann |
added explicit print translation for nat_case
|
file |
diff |
annotate
|
| 2006-10-02 |
haftmann |
added code generator names for nat_rec and nat_case
|
file |
diff |
annotate
|
| 2006-09-26 |
haftmann |
renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
|
file |
diff |
annotate
|
| 2006-09-25 |
haftmann |
refinements in codegen serializer
|
file |
diff |
annotate
|
| 2006-09-20 |
haftmann |
name shifts
|
file |
diff |
annotate
|
| 2006-09-19 |
haftmann |
added operational equality
|
file |
diff |
annotate
|
| 2006-08-14 |
haftmann |
simplified code generator setup
|
file |
diff |
annotate
|
| 2006-08-08 |
haftmann |
cleanup code generation for Numerals
|
file |
diff |
annotate
|
| 2006-06-14 |
haftmann |
slight adaption for code generator
|
file |
diff |
annotate
|
| 2006-06-13 |
paulson |
new results
|
file |
diff |
annotate
|
| 2006-05-05 |
wenzelm |
axiomatization;
|
file |
diff |
annotate
|
| 2006-01-17 |
haftmann |
substantial improvements in code generator
|
file |
diff |
annotate
|
| 2006-01-11 |
paulson |
tidied, and giving theorems names
|
file |
diff |
annotate
|
| 2005-09-28 |
wenzelm |
more finalconsts;
|
file |
diff |
annotate
|
| 2005-09-22 |
nipkow |
renamed rules to iprover
|
file |
diff |
annotate
|
| 2005-07-13 |
paulson |
generlization of some "nat" theorems
|
file |
diff |
annotate
|
| 2005-07-07 |
nipkow |
linear arithmetic now takes "&" in assumptions apart.
|
file |
diff |
annotate
|
| 2005-07-01 |
berghofe |
Moved some code lemmas from Main to Nat.
|
file |
diff |
annotate
|
| 2005-05-04 |
nipkow |
Fixing a problem with lin.arith.
|
file |
diff |
annotate
|
| 2005-02-21 |
nipkow |
comprehensive cleanup, replacing sumr by setsum
|
file |
diff |
annotate
|
| 2004-12-15 |
paulson |
removal of archaic Abs/Rep proofs
|
file |
diff |
annotate
|
| 2004-11-29 |
paulson |
converted to Isar script, simplifying some results
|
file |
diff |
annotate
|
| 2004-11-13 |
nipkow |
More lemmas
|
file |
diff |
annotate
|
| 2004-10-19 |
paulson |
converted some induct_tac to induct
|
file |
diff |
annotate
|
| 2004-08-18 |
nipkow |
import -> imports
|
file |
diff |
annotate
|
| 2004-08-16 |
nipkow |
New theory header syntax.
|
file |
diff |
annotate
|
| 2004-05-12 |
nipkow |
fixed latex problems
|
file |
diff |
annotate
|
| 2004-05-11 |
obua |
changes made due to new Ring_and_Field theory
|
file |
diff |
annotate
|
| 2004-05-01 |
wenzelm |
tuned instance statements;
|
file |
diff |
annotate
|
| 2004-01-09 |
paulson |
Defining the type class "ringpower" and deleting superseded theorems for
|
file |
diff |
annotate
|
| 2004-01-06 |
paulson |
Ring_and_Field now requires axiom add_left_imp_eq for semirings.
|
file |
diff |
annotate
|
| 2003-12-27 |
paulson |
re-organized numeric lemmas
|
file |
diff |
annotate
|
| 2003-12-19 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| 2003-11-25 |
paulson |
More refinements to Ring_and_Field and numerics. Conversion of Divides_lemmas
|
file |
diff |
annotate
|
| 2003-11-24 |
paulson |
conversion of integers to use Ring_and_Field;
|
file |
diff |
annotate
|
| 2003-11-21 |
paulson |
HOL: installation of Ring_and_Field as the basis for Naturals and Reals
|
file |
diff |
annotate
|
| 2003-09-26 |
paulson |
misc tidying
|
file |
diff |
annotate
|
| 2003-09-22 |
berghofe |
Improved efficiency of code generated for + and -
|
file |
diff |
annotate
|
| 2003-07-24 |
paulson |
declarations moved from PreList.thy
|
file |
diff |
annotate
|
| 2002-09-30 |
nipkow |
modified induct method
|
file |
diff |
annotate
|
| 2002-09-26 |
paulson |
Converted Fun to Isar style.
|
file |
diff |
annotate
|
| 2002-08-05 |
berghofe |
- Converted to new theory format
|
file |
diff |
annotate
|
| 2001-12-01 |
wenzelm |
renamed class "term" to "type" (actually "HOL.type");
|
file |
diff |
annotate
|
| 2001-07-25 |
paulson |
partial restructuring to reduce dependence on Axiom of Choice
|
file |
diff |
annotate
|
| 2001-05-22 |
berghofe |
Inductive definitions are now introduced earlier in the theory hierarchy.
|
file |
diff |
annotate
|
| 2001-02-15 |
oheimb |
added nat as instance of new wellorder axclass
|
file |
diff |
annotate
|
| 2000-11-10 |
wenzelm |
added axclass power (from HOL.thy);
|
file |
diff |
annotate
|
| 2000-07-24 |
wenzelm |
rearranged setup of arithmetic procedures, avoiding global reference values;
|
file |
diff |
annotate
|
| 1999-10-04 |
wenzelm |
removed DatatypePackage.setup;
|
file |
diff |
annotate
|
| 1998-10-21 |
berghofe |
Changed syntax of rep_datatype.
|
file |
diff |
annotate
|
| 1998-09-18 |
paulson |
updated comments
|
file |
diff |
annotate
|
| 1998-07-24 |
berghofe |
Declaration of type 'nat' as a datatype (this allows usage of
|
file |
diff |
annotate
|
| 1998-02-20 |
nipkow |
Congruence rules use == in premises now.
|
file |
diff |
annotate
|
| 1998-02-09 |
nipkow |
Replaced ALLNEWSUBGOALS by THEN_ALL_NEW
|
file |
diff |
annotate
|
| 1997-11-03 |
wenzelm |
nat datatype_info moved to Nat.thy;
|
file |
diff |
annotate
|
| 1997-05-30 |
paulson |
Overloading of "^" requires new type class "power", with types "nat" and
|
file |
diff |
annotate
|
| 1997-02-12 |
nipkow |
New class "order" and accompanying changes.
|
file |
diff |
annotate
|
| 1997-01-23 |
wenzelm |
removed \<mu> syntax;
|
file |
diff |
annotate
|
| 1996-12-13 |
oheimb |
adaptions for symbol font
|
file |
diff |
annotate
|