| 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
|