| Wed, 28 Mar 2007 10:47:19 +0200 |
berghofe |
Improved code generator for characters: now handles
|
changeset |
files
|
| Wed, 28 Mar 2007 01:55:18 +0200 |
urbanc |
tuned proofs (taking full advantage of nominal_inductive)
|
changeset |
files
|
| Wed, 28 Mar 2007 01:29:43 +0200 |
urbanc |
adapted to nominal_inductive infrastructure
|
changeset |
files
|
| Wed, 28 Mar 2007 01:09:23 +0200 |
urbanc |
made the type sets instance of the "cp" type-class
|
changeset |
files
|
| Tue, 27 Mar 2007 19:39:40 +0200 |
urbanc |
added extended the lemma for equivariance of freshness
|
changeset |
files
|
| Tue, 27 Mar 2007 19:13:28 +0200 |
urbanc |
adapted to nominal_inductive
|
changeset |
files
|
| Tue, 27 Mar 2007 18:28:22 +0200 |
urbanc |
adapted to new nominal_inductive infrastructure
|
changeset |
files
|
| Tue, 27 Mar 2007 17:57:42 +0200 |
berghofe |
Adapted to new syntax of nominal_inductive.
|
changeset |
files
|
| Tue, 27 Mar 2007 17:57:05 +0200 |
berghofe |
Adapted to changes in nominal_inductive.
|
changeset |
files
|
| Tue, 27 Mar 2007 17:55:09 +0200 |
berghofe |
Implemented proof of strong induction rule.
|
changeset |
files
|
| Tue, 27 Mar 2007 17:54:37 +0200 |
berghofe |
Exported perm_of_pair, mk_not_sym, and perm_simproc.
|
changeset |
files
|
| Tue, 27 Mar 2007 12:28:42 +0200 |
haftmann |
cleaned up HOL/ex/Code*.thy
|
changeset |
files
|
| Tue, 27 Mar 2007 09:19:37 +0200 |
haftmann |
fixed document preparation
|
changeset |
files
|
| Mon, 26 Mar 2007 16:35:33 +0200 |
krauss |
fixed problem with mutual recursion
|
changeset |
files
|
| Mon, 26 Mar 2007 14:54:45 +0200 |
haftmann |
cleaned up Library/ and ex/
|
changeset |
files
|
| Mon, 26 Mar 2007 14:53:07 +0200 |
haftmann |
minimal intro rules
|
changeset |
files
|
| Mon, 26 Mar 2007 14:53:06 +0200 |
haftmann |
exported interface for intro rules
|
changeset |
files
|
| Mon, 26 Mar 2007 14:53:05 +0200 |
haftmann |
moved Eval theory to library
|
changeset |
files
|
| Mon, 26 Mar 2007 14:53:04 +0200 |
haftmann |
Eval theory
|
changeset |
files
|
| Mon, 26 Mar 2007 14:53:03 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Mon, 26 Mar 2007 14:53:02 +0200 |
haftmann |
importing Eval theory
|
changeset |
files
|
| Mon, 26 Mar 2007 14:53:01 +0200 |
haftmann |
naming tuned
|
changeset |
files
|
| Mon, 26 Mar 2007 14:53:00 +0200 |
haftmann |
cleaned up Library( and ex/
|
changeset |
files
|
| Mon, 26 Mar 2007 12:48:30 +0200 |
paulson |
Clause cache is now in theory data.
|
changeset |
files
|
| Mon, 26 Mar 2007 12:46:27 +0200 |
paulson |
"generalize" now replaces ugly mes_XXX generated symbols by 1-letter identifiers.
|
changeset |
files
|
| Sun, 25 Mar 2007 15:15:07 +0200 |
urbanc |
moving lemmas into appropriate sections
|
changeset |
files
|
| Fri, 23 Mar 2007 12:06:41 +0100 |
haftmann |
fixed typing bug in generated code
|
changeset |
files
|
| Fri, 23 Mar 2007 12:05:43 +0100 |
haftmann |
fixed typing bug in generated code
|
changeset |
files
|
| Fri, 23 Mar 2007 10:50:03 +0100 |
urbanc |
added the permutation operation on options to the list of equivariance lemmas
|
changeset |
files
|
| Fri, 23 Mar 2007 09:46:22 +0100 |
haftmann |
dropped
|
changeset |
files
|
| Fri, 23 Mar 2007 09:40:57 +0100 |
haftmann |
added empty cases
|
changeset |
files
|
| Fri, 23 Mar 2007 09:40:53 +0100 |
haftmann |
added concept for term constructors
|
changeset |
files
|
| Fri, 23 Mar 2007 09:40:50 +0100 |
haftmann |
tuned
|
changeset |
files
|
| Fri, 23 Mar 2007 09:40:49 +0100 |
haftmann |
two further properties about lists
|
changeset |
files
|
| Fri, 23 Mar 2007 09:40:47 +0100 |
haftmann |
removed outdated example
|
changeset |
files
|
| Fri, 23 Mar 2007 09:40:45 +0100 |
haftmann |
fixed typo
|
changeset |
files
|
| Fri, 23 Mar 2007 09:40:43 +0100 |
haftmann |
added some sketches about library functions
|
changeset |
files
|
| Thu, 22 Mar 2007 16:53:37 +0100 |
krauss |
fixed function syntax
|
changeset |
files
|
| Thu, 22 Mar 2007 16:34:03 +0100 |
krauss |
fixed function syntax
|
changeset |
files
|
| Thu, 22 Mar 2007 14:26:05 +0100 |
urbanc |
corrected the lemmas min_nat_eqvt and min_int_eqvt
|
changeset |
files
|
| Thu, 22 Mar 2007 14:03:30 +0100 |
haftmann |
fixed code generator setup
|
changeset |
files
|
| Thu, 22 Mar 2007 13:36:57 +0100 |
krauss |
made function syntax strict, requiring | to separate equations; cleanup
|
changeset |
files
|
| Thu, 22 Mar 2007 13:36:56 +0100 |
krauss |
fixed problem with the construction of mutual simp rules
|
changeset |
files
|
| Thu, 22 Mar 2007 13:36:55 +0100 |
krauss |
cleanup
|
changeset |
files
|
| Thu, 22 Mar 2007 11:17:32 +0100 |
urbanc |
clarified an error-message
|
changeset |
files
|
| Thu, 22 Mar 2007 10:35:12 +0100 |
urbanc |
tuned some proofs
|
changeset |
files
|
| Wed, 21 Mar 2007 16:07:40 +0100 |
krauss |
added another rule for simultaneous induction, and lemmas for zip
|
changeset |
files
|
| Wed, 21 Mar 2007 16:06:15 +0100 |
krauss |
Unified function syntax
|
changeset |
files
|
| Wed, 21 Mar 2007 13:58:36 +0100 |
paulson |
Numerous bug fixes. Type clauses distinguished from empty clauses. Working proof reduction.
|
changeset |
files
|
| Wed, 21 Mar 2007 08:07:19 +0100 |
haftmann |
added example file
|
changeset |
files
|
| Tue, 20 Mar 2007 21:21:38 +0100 |
gagern |
Better documentation path rewriting for src dir, used in tarball build.
|
changeset |
files
|
| Tue, 20 Mar 2007 20:42:14 +0100 |
gagern |
Changed AnnoMaLy build process from CVS to tarball sources.
|
changeset |
files
|
| Tue, 20 Mar 2007 17:07:23 +0100 |
krauss |
simplified "eval" oracle method
|
changeset |
files
|
| Tue, 20 Mar 2007 15:52:43 +0100 |
haftmann |
updated keywords
|
changeset |
files
|
| Tue, 20 Mar 2007 15:52:42 +0100 |
haftmann |
added theory dependency graph
|
changeset |
files
|
| Tue, 20 Mar 2007 15:52:41 +0100 |
haftmann |
improved treatment of defining equations stemming from specification tools
|
changeset |
files
|
| Tue, 20 Mar 2007 15:52:40 +0100 |
haftmann |
added instance for lattice
|
changeset |
files
|
| Tue, 20 Mar 2007 15:52:39 +0100 |
haftmann |
dropped OrderedGroup.ML
|
changeset |
files
|
| Tue, 20 Mar 2007 15:52:38 +0100 |
haftmann |
added class "default" and expansion axioms for undefined
|
changeset |
files
|
| Tue, 20 Mar 2007 15:52:37 +0100 |
haftmann |
switched exception from arbitrary to undefined
|
changeset |
files
|