| Mon, 16 Dec 2002 13:43:11 +0100 |
berghofe |
Added mk_int and mk_list.
|
changeset |
files
|
| Mon, 16 Dec 2002 11:18:35 +0100 |
berghofe |
Code generator for datatypes now also generates suitable term_of functions (when
|
changeset |
files
|
| Mon, 16 Dec 2002 11:17:16 +0100 |
berghofe |
- Added mode reference variable (may be used to switch on and off specific
|
changeset |
files
|
| Fri, 13 Dec 2002 18:14:25 +0100 |
oheimb |
cent/currency: changed from wasysym to textcomp because of PDF problems
|
changeset |
files
|
| Fri, 13 Dec 2002 16:49:08 +0100 |
paulson |
trace_unify_fail
|
changeset |
files
|
| Fri, 13 Dec 2002 16:48:20 +0100 |
paulson |
integer induction rules
|
changeset |
files
|
| Fri, 13 Dec 2002 14:20:47 +0100 |
berghofe |
size_of_proof no longer includes size_of_term
|
changeset |
files
|
| Fri, 13 Dec 2002 13:47:13 +0100 |
paulson |
deleted redundant line
|
changeset |
files
|
| Thu, 12 Dec 2002 11:38:18 +0100 |
paulson |
Better treatment of equality in premises of inductive definitions. Less
|
changeset |
files
|
| Thu, 12 Dec 2002 11:33:48 +0100 |
ballarin |
Fixed error that affected document preperation.
|
changeset |
files
|
| Wed, 11 Dec 2002 10:12:48 +0100 |
ballarin |
HOL/GroupTheory/Summation.thy added: summation operator for abelian groups.
|
changeset |
files
|
| Tue, 10 Dec 2002 10:40:32 +0100 |
berghofe |
Added size_of_proof.
|
changeset |
files
|
| Mon, 09 Dec 2002 10:38:56 +0100 |
ballarin |
Fixed bug in simpdata.ML that prevented the use of congruence rules from a
|
changeset |
files
|
| Fri, 06 Dec 2002 15:16:30 +0100 |
oheimb |
corrected swallowing of newlines after end-of-ignore
|
changeset |
files
|
| Fri, 06 Dec 2002 11:09:02 +0100 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Thu, 05 Dec 2002 18:44:16 +0100 |
kleing |
for dvi target
|
changeset |
files
|
| Thu, 05 Dec 2002 17:12:07 +0100 |
kleing |
exercise collection
|
changeset |
files
|
| Fri, 29 Nov 2002 14:26:55 +0100 |
ballarin |
Incompatibility with SML/NJ fixed.
|
changeset |
files
|
| Fri, 29 Nov 2002 09:48:28 +0100 |
nipkow |
added a few lemmas
|
changeset |
files
|
| Thu, 28 Nov 2002 15:44:34 +0100 |
ballarin |
Transitivity reasoner renamed to linorder.ML. README updated.
|
changeset |
files
|
| Thu, 28 Nov 2002 10:50:42 +0100 |
ballarin |
HOL-Algebra partially ported to Isar.
|
changeset |
files
|
| Wed, 27 Nov 2002 17:25:41 +0100 |
berghofe |
prop_of now returns proposition in beta-eta normal form.
|
changeset |
files
|
| Wed, 27 Nov 2002 17:25:04 +0100 |
berghofe |
- tuned beta_eta_convert
|
changeset |
files
|
| Wed, 27 Nov 2002 17:23:19 +0100 |
berghofe |
Correctness proofs are now modular, too.
|
changeset |
files
|
| Wed, 27 Nov 2002 17:22:18 +0100 |
berghofe |
Parameters in definitions are now renamed to avoid clashes with
|
changeset |
files
|
| Wed, 27 Nov 2002 17:20:49 +0100 |
berghofe |
default_output now escapes \'s more carefully.
|
changeset |
files
|
| Wed, 27 Nov 2002 17:17:53 +0100 |
berghofe |
Added XML parser (useful for parsing PGIP / PGML).
|
changeset |
files
|
| Wed, 27 Nov 2002 17:16:47 +0100 |
berghofe |
Added some functions for processing PGIP (thanks to David Aspinall).
|
changeset |
files
|
| Wed, 27 Nov 2002 17:11:38 +0100 |
berghofe |
Fixed bug in consts_code section.
|
changeset |
files
|
| Wed, 27 Nov 2002 17:07:05 +0100 |
berghofe |
Replaced some blasts by rules.
|
changeset |
files
|
| Wed, 27 Nov 2002 17:06:47 +0100 |
berghofe |
Changed format of realizers / correctness proofs.
|
changeset |
files
|
| Mon, 25 Nov 2002 20:32:29 +0100 |
nipkow |
renamed a few constants
|
changeset |
files
|
| Thu, 21 Nov 2002 17:40:11 +0100 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Wed, 20 Nov 2002 10:43:20 +0100 |
paulson |
textual tweak
|
changeset |
files
|
| Tue, 19 Nov 2002 10:41:20 +0100 |
paulson |
stylistic tweaks
|
changeset |
files
|
| Mon, 18 Nov 2002 14:51:44 +0100 |
nipkow |
beautification
|
changeset |
files
|
| Sun, 17 Nov 2002 23:43:53 +0100 |
berghofe |
Fixed small bug that caused some definitions to be "forgotten".
|
changeset |
files
|
| Sat, 16 Nov 2002 23:01:59 +0100 |
kleing |
beautified "match"
|
changeset |
files
|
| Sat, 16 Nov 2002 22:54:39 +0100 |
kleing |
beautified "match"
|
changeset |
files
|
| Fri, 15 Nov 2002 18:02:25 +0100 |
nipkow |
added zdvd_iff_zmod_eq_0
|
changeset |
files
|
| Wed, 13 Nov 2002 15:36:36 +0100 |
berghofe |
Improved function decompose.
|
changeset |
files
|
| Wed, 13 Nov 2002 15:36:06 +0100 |
berghofe |
- exported functions etype_of and mk_typ
|
changeset |
files
|
| Wed, 13 Nov 2002 15:35:15 +0100 |
berghofe |
Fixed name clash problem in forall_elim_var.
|
changeset |
files
|
| Wed, 13 Nov 2002 15:34:35 +0100 |
berghofe |
Added simple_prove_goal_cterm.
|
changeset |
files
|
| Wed, 13 Nov 2002 15:34:01 +0100 |
berghofe |
Removed (now unneeded) declarations of realizers for bar induction.
|
changeset |
files
|
| Wed, 13 Nov 2002 15:32:41 +0100 |
berghofe |
New package for constructing realizers for introduction and elimination
|
changeset |
files
|
| Wed, 13 Nov 2002 15:31:14 +0100 |
berghofe |
- No longer applies norm_hhf_rule
|
changeset |
files
|
| Wed, 13 Nov 2002 15:28:41 +0100 |
berghofe |
prove_goal' -> Goal.simple_prove_goal_cterm
|
changeset |
files
|
| Wed, 13 Nov 2002 15:27:27 +0100 |
berghofe |
name_of_type now replaces non-identifiers by dummy names.
|
changeset |
files
|
| Wed, 13 Nov 2002 15:26:19 +0100 |
berghofe |
Added inductive_realizer.
|
changeset |
files
|
| Wed, 13 Nov 2002 15:25:17 +0100 |
berghofe |
Added InductiveRealizer package.
|
changeset |
files
|
| Wed, 13 Nov 2002 15:24:42 +0100 |
berghofe |
Transitive closure is now defined inductively as well.
|
changeset |
files
|
| Sat, 09 Nov 2002 00:12:25 +0100 |
kleing |
Hoare.ML -> hoare.ML
|
changeset |
files
|
| Fri, 08 Nov 2002 10:34:40 +0100 |
paulson |
Polishing.
|
changeset |
files
|
| Fri, 08 Nov 2002 10:28:29 +0100 |
paulson |
generalized wf_on_unit to wf_on_any_0
|
changeset |
files
|
| Thu, 07 Nov 2002 12:35:34 +0100 |
nipkow |
added raw proof blocks
|
changeset |
files
|
| Thu, 07 Nov 2002 09:26:44 +0100 |
nipkow |
small improvements
|
changeset |
files
|
| Thu, 07 Nov 2002 09:08:25 +0100 |
nipkow |
added show_main_goal
|
changeset |
files
|
| Wed, 06 Nov 2002 14:02:18 +0100 |
nipkow |
Hoare.ML -> hoare.ML
|
changeset |
files
|
| Wed, 06 Nov 2002 14:01:38 +0100 |
nipkow |
a new pointer example and some syntactic sugar
|
changeset |
files
|