| Mon, 14 May 2007 17:37:31 +0200 |
huffman |
new lemmas
|
changeset |
files
|
| Mon, 14 May 2007 13:24:22 +0200 |
webertj |
ProofGeneral: Find Theorems search form
|
changeset |
files
|
| Mon, 14 May 2007 12:52:56 +0200 |
haftmann |
reorganized float arithmetic
|
changeset |
files
|
| Mon, 14 May 2007 12:52:54 +0200 |
haftmann |
fixed IntInf ambiguity
|
changeset |
files
|
| Mon, 14 May 2007 09:33:18 +0200 |
huffman |
remove redundant lemmas
|
changeset |
files
|
| Mon, 14 May 2007 09:27:24 +0200 |
huffman |
remove redundant lemmas
|
changeset |
files
|
| Mon, 14 May 2007 09:16:47 +0200 |
huffman |
remove redundant lemmas
|
changeset |
files
|
| Mon, 14 May 2007 09:11:30 +0200 |
huffman |
remove redundant lemmas
|
changeset |
files
|
| Mon, 14 May 2007 08:15:13 +0200 |
huffman |
cleaned up
|
changeset |
files
|
| Mon, 14 May 2007 08:12:38 +0200 |
huffman |
tuned
|
changeset |
files
|
| Sun, 13 May 2007 20:05:42 +0200 |
huffman |
define roots of negative reals so that many lemmas no longer require side conditions; simplification solves more goals than previously
|
changeset |
files
|
| Sun, 13 May 2007 19:15:36 +0200 |
huffman |
add lemma power_eq_imp_eq_base
|
changeset |
files
|
| Sun, 13 May 2007 18:16:49 +0200 |
haftmann |
added module int
|
changeset |
files
|
| Sun, 13 May 2007 18:15:30 +0200 |
haftmann |
dropped legacy
|
changeset |
files
|
| Sun, 13 May 2007 18:15:28 +0200 |
haftmann |
removed module rat.ML
|
changeset |
files
|
| Sun, 13 May 2007 18:15:26 +0200 |
haftmann |
whitespace tuned
|
changeset |
files
|
| Sun, 13 May 2007 18:15:25 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Sun, 13 May 2007 18:15:24 +0200 |
haftmann |
fixed omission
|
changeset |
files
|
| Sun, 13 May 2007 18:15:23 +0200 |
haftmann |
tuned setup
|
changeset |
files
|
| Sun, 13 May 2007 18:15:22 +0200 |
haftmann |
refined module rat
|
changeset |
files
|
| Sun, 13 May 2007 18:15:21 +0200 |
haftmann |
added modules rat.ML and int.ML
|
changeset |
files
|
| Sun, 13 May 2007 09:23:27 +0200 |
nipkow |
Removed junk
|
changeset |
files
|
| Sun, 13 May 2007 07:11:21 +0200 |
nipkow |
Got rid of listsp
|
changeset |
files
|
| Sun, 13 May 2007 04:38:24 +0200 |
huffman |
removed redundant lemmas
|
changeset |
files
|
| Sat, 12 May 2007 18:16:30 +0200 |
huffman |
add lemma additive.setsum
|
changeset |
files
|
| Fri, 11 May 2007 20:47:30 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Fri, 11 May 2007 20:07:00 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|
| Fri, 11 May 2007 18:49:15 +0200 |
wenzelm |
proper type for fun/arg_cong_rule;
|
changeset |
files
|
| Fri, 11 May 2007 18:47:08 +0200 |
wenzelm |
added fun/arg_cong_rule;
|
changeset |
files
|
| Fri, 11 May 2007 18:46:50 +0200 |
wenzelm |
unified names: foo_conv;
|
changeset |
files
|
| Fri, 11 May 2007 17:54:36 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Fri, 11 May 2007 15:37:42 +0200 |
krauss |
added fun flip f x y = f y x
|
changeset |
files
|
| Fri, 11 May 2007 03:31:12 +0200 |
huffman |
generalize setsum lemmas from semiring_0_cancel to semiring_0
|
changeset |
files
|
| Fri, 11 May 2007 01:07:10 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Fri, 11 May 2007 00:43:46 +0200 |
wenzelm |
bang_facts: warning;
|
changeset |
files
|
| Fri, 11 May 2007 00:43:45 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Thu, 10 May 2007 22:11:38 +0200 |
haftmann |
(class target)
|
changeset |
files
|
| Thu, 10 May 2007 22:11:37 +0200 |
haftmann |
cleaned up
|
changeset |
files
|
| Thu, 10 May 2007 22:11:36 +0200 |
haftmann |
beta/eta conversion after preprocessor
|
changeset |
files
|
| Thu, 10 May 2007 22:11:35 +0200 |
haftmann |
fixed typo
|
changeset |
files
|
| Thu, 10 May 2007 18:10:32 +0200 |
wenzelm |
more conversions;
|
changeset |
files
|
| Thu, 10 May 2007 15:51:59 +0200 |
berghofe |
Moved extraction_expand declaration of listall_def outside of definition.
|
changeset |
files
|
| Thu, 10 May 2007 15:50:56 +0200 |
berghofe |
Adapted to new naming scheme for definitions.
|
changeset |
files
|
| Thu, 10 May 2007 15:50:28 +0200 |
berghofe |
Changed name of raw definition.
|
changeset |
files
|
| Thu, 10 May 2007 15:49:31 +0200 |
berghofe |
Name of ML function "not" is now qualified in order to avoid
|
changeset |
files
|
| Thu, 10 May 2007 10:22:17 +0200 |
haftmann |
consts in consts_code Isar commands are now referred to by usual term syntax
|
changeset |
files
|
| Thu, 10 May 2007 10:21:50 +0200 |
haftmann |
size [nat] is identity
|
changeset |
files
|
| Thu, 10 May 2007 10:21:48 +0200 |
haftmann |
explicit import of Datatype.thy due to hook bootstrap problem
|
changeset |
files
|
| Thu, 10 May 2007 10:21:47 +0200 |
haftmann |
localized Sup/Inf
|
changeset |
files
|
| Thu, 10 May 2007 10:21:46 +0200 |
haftmann |
localized Min/Max
|
changeset |
files
|
| Thu, 10 May 2007 10:21:44 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Thu, 10 May 2007 04:06:56 +0200 |
huffman |
fix proofs
|
changeset |
files
|
| Thu, 10 May 2007 03:11:03 +0200 |
huffman |
remove redundant lemmas
|
changeset |
files
|
| Thu, 10 May 2007 03:07:26 +0200 |
huffman |
lemmas iszero_(h)complex_number_of are no longer needed
|
changeset |
files
|
| Thu, 10 May 2007 03:00:15 +0200 |
huffman |
instance real_algebra_1 < ring_char_0
|
changeset |
files
|
| Thu, 10 May 2007 02:51:53 +0200 |
huffman |
new axclass ring_char_0 for rings with characteristic 0, used for of_int_eq_iff and related lemmas
|
changeset |
files
|
| Thu, 10 May 2007 00:39:56 +0200 |
wenzelm |
moved conversions to structure Conv;
|
changeset |
files
|
| Thu, 10 May 2007 00:39:55 +0200 |
wenzelm |
added dest_fun/fun2/arg1;
|
changeset |
files
|
| Thu, 10 May 2007 00:39:54 +0200 |
wenzelm |
tuned argument_type_of;
|
changeset |
files
|
| Thu, 10 May 2007 00:39:53 +0200 |
wenzelm |
added destructors from drule.ML;
|
changeset |
files
|
| Thu, 10 May 2007 00:39:52 +0200 |
wenzelm |
moved some operations to more_thm.ML and conv.ML;
|
changeset |
files
|
| Thu, 10 May 2007 00:39:51 +0200 |
wenzelm |
Conversions: primitive equality reasoning (from drule.ML);
|
changeset |
files
|
| Thu, 10 May 2007 00:39:50 +0200 |
wenzelm |
added conv.ML;
|
changeset |
files
|
| Thu, 10 May 2007 00:39:49 +0200 |
wenzelm |
Thm.match;
|
changeset |
files
|
| Thu, 10 May 2007 00:39:48 +0200 |
wenzelm |
moved some Drule operations to Thm (see more_thm.ML);
|
changeset |
files
|
| Thu, 10 May 2007 00:39:46 +0200 |
wenzelm |
Thm.first_order_match;
|
changeset |
files
|
| Thu, 10 May 2007 00:39:45 +0200 |
wenzelm |
moved conversions to structure Conv;
|
changeset |
files
|
| Wed, 09 May 2007 23:28:18 +0200 |
krauss |
"fun" command: Changed pattern compatibility proof back from "simp_all" to the slower but more robust "auto"
|
changeset |
files
|
| Wed, 09 May 2007 22:14:26 +0200 |
huffman |
add lemma norm_diff_ineq; shorten other proofs
|
changeset |
files
|
| Wed, 09 May 2007 19:37:22 +0200 |
wenzelm |
removed Complex/ComplexBin.thy;
|
changeset |
files
|
| Wed, 09 May 2007 19:37:21 +0200 |
wenzelm |
tuned ML setup;
|
changeset |
files
|
| Wed, 09 May 2007 19:37:20 +0200 |
wenzelm |
tuned syntax;
|
changeset |
files
|
| Wed, 09 May 2007 19:37:19 +0200 |
wenzelm |
eliminated unnamed infixes;
|
changeset |
files
|
| Wed, 09 May 2007 19:37:18 +0200 |
wenzelm |
removed unused mk_cond_defpair;
|
changeset |
files
|
| Wed, 09 May 2007 19:20:00 +0200 |
wenzelm |
simp_depth: now proper value in simpset (prevents problems with lost exception trace, enables multi-threaded simplification);
|
changeset |
files
|
| Wed, 09 May 2007 18:58:03 +0200 |
huffman |
remove empty, unused theory
|
changeset |
files
|
| Wed, 09 May 2007 18:26:40 +0200 |
huffman |
remove redundant lemmas
|
changeset |
files
|
| Wed, 09 May 2007 18:25:44 +0200 |
huffman |
add lemma hnorm_hyperpow
|
changeset |
files
|
| Wed, 09 May 2007 18:25:21 +0200 |
huffman |
add lemma of_hypreal_hyperpow
|
changeset |
files
|
| Wed, 09 May 2007 07:53:08 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Wed, 09 May 2007 07:53:06 +0200 |
haftmann |
moved recfun_codegen.ML to Code_Generator.thy
|
changeset |
files
|
| Wed, 09 May 2007 07:53:04 +0200 |
haftmann |
continued
|
changeset |
files
|
| Wed, 09 May 2007 01:56:59 +0200 |
huffman |
remove redundant lemmas
|
changeset |
files
|
| Wed, 09 May 2007 01:26:04 +0200 |
huffman |
hcomplex_of_hypreal abbreviates of_hypreal; removed redundant lemmas
|
changeset |
files
|
| Wed, 09 May 2007 00:57:46 +0200 |
huffman |
add lemma hnorm_divide
|
changeset |
files
|
| Wed, 09 May 2007 00:33:12 +0200 |
huffman |
add lemmas abs_hnorm_cancel, hnorm_of_hypreal
|
changeset |
files
|
| Wed, 09 May 2007 00:27:36 +0200 |
huffman |
add lemmas norm_add_less, norm_mult_less
|
changeset |
files
|
| Tue, 08 May 2007 23:52:15 +0200 |
huffman |
add lemma Standard_hyperpow
|
changeset |
files
|
| Tue, 08 May 2007 21:02:26 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 08 May 2007 19:15:35 +0200 |
huffman |
add of_hypreal constant with lemmas
|
changeset |
files
|
| Tue, 08 May 2007 18:23:37 +0200 |
huffman |
add lemmas norm_number_of, norm_of_int, norm_of_nat
|
changeset |
files
|
| Tue, 08 May 2007 17:41:35 +0200 |
wenzelm |
quoted 'declaration';
|
changeset |
files
|
| Tue, 08 May 2007 17:40:22 +0200 |
wenzelm |
simplified pretty_thm(_legacy);
|
changeset |
files
|
| Tue, 08 May 2007 17:40:21 +0200 |
wenzelm |
is_sid: include '::';
|
changeset |
files
|
| Tue, 08 May 2007 17:40:20 +0200 |
wenzelm |
tuned ProofDisplay.pretty_full_theory;
|
changeset |
files
|
| Tue, 08 May 2007 17:40:18 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 08 May 2007 15:37:27 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Tue, 08 May 2007 15:37:19 +0200 |
wenzelm |
simplified context data;
|
changeset |
files
|
| Tue, 08 May 2007 15:36:39 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 08 May 2007 15:01:33 +0200 |
wenzelm |
legacy_intern_skolem: legacy_feature;
|
changeset |
files
|
| Tue, 08 May 2007 15:01:31 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Tue, 08 May 2007 15:01:30 +0200 |
wenzelm |
renamed call_atp to sledgehammer;
|
changeset |
files
|
| Tue, 08 May 2007 15:01:29 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Tue, 08 May 2007 15:01:28 +0200 |
wenzelm |
tuned context data;
|
changeset |
files
|
| Tue, 08 May 2007 08:21:39 +0200 |
haftmann |
ML adaptions
|
changeset |
files
|
| Tue, 08 May 2007 05:30:10 +0200 |
huffman |
clean up complex norm proofs, remove redundant lemmas
|
changeset |
files
|
| Tue, 08 May 2007 05:06:54 +0200 |
huffman |
remove redundant lemmas
|
changeset |
files
|
| Tue, 08 May 2007 05:06:04 +0200 |
huffman |
fix proof of hypreal_sqrt_sum_squares_ge1
|
changeset |
files
|
| Tue, 08 May 2007 04:56:28 +0200 |
huffman |
add lemma real_sqrt_sum_squares_triangle_ineq
|
changeset |
files
|
| Tue, 08 May 2007 04:55:19 +0200 |
huffman |
add lemma abs_norm_cancel
|
changeset |
files
|
| Tue, 08 May 2007 03:03:23 +0200 |
huffman |
cleaned up
|
changeset |
files
|
| Tue, 08 May 2007 01:40:30 +0200 |
urbanc |
polished some proofs
|
changeset |
files
|
| Tue, 08 May 2007 01:10:55 +0200 |
huffman |
add lemmas power2_le_imp_le and power2_less_imp_less
|
changeset |
files
|
| Tue, 08 May 2007 00:50:55 +0200 |
huffman |
add lemma power_less_imp_less_base
|
changeset |
files
|
| Mon, 07 May 2007 23:07:04 +0200 |
huffman |
clean up RealVector classes
|
changeset |
files
|
| Mon, 07 May 2007 16:46:42 +0200 |
paulson |
First-order variant of the fully-typed translation
|
changeset |
files
|
| Mon, 07 May 2007 14:20:32 +0200 |
haftmann |
added further equality example
|
changeset |
files
|
| Mon, 07 May 2007 09:58:07 +0200 |
haftmann |
changed 'code nofunc' to 'code func del'
|
changeset |
files
|
| Mon, 07 May 2007 00:52:25 +0200 |
wenzelm |
* Context data interfaces;
|
changeset |
files
|
| Mon, 07 May 2007 00:50:09 +0200 |
wenzelm |
simplified DataFun interfaces: removed name/print, use adhoc value for uninitialized data, init only required for impure data;
|
changeset |
files
|
| Mon, 07 May 2007 00:49:59 +0200 |
wenzelm |
simplified DataFun interfaces;
|
changeset |
files
|
| Sun, 06 May 2007 21:50:17 +0200 |
haftmann |
changed code generator invocation syntax
|
changeset |
files
|
| Sun, 06 May 2007 21:49:44 +0200 |
haftmann |
PreList imports RecDef
|
changeset |
files
|
| Sun, 06 May 2007 21:49:32 +0200 |
haftmann |
dropped legacy ML binding
|
changeset |
files
|
| Sun, 06 May 2007 21:49:29 +0200 |
haftmann |
added auxiliary lemmas for proof tools
|
changeset |
files
|
| Sun, 06 May 2007 21:49:27 +0200 |
haftmann |
dropped preorders, unified syntax
|
changeset |
files
|
| Sun, 06 May 2007 21:49:26 +0200 |
haftmann |
minimal import
|
changeset |
files
|
| Sun, 06 May 2007 21:49:24 +0200 |
haftmann |
dropped HOL.ML
|
changeset |
files
|
| Sun, 06 May 2007 21:49:23 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Sun, 06 May 2007 18:07:06 +0200 |
wenzelm |
updated Alice version;
|
changeset |
files
|
| Sun, 06 May 2007 18:07:04 +0200 |
wenzelm |
IntInf.fromInt;
|
changeset |
files
|
| Sun, 06 May 2007 13:33:39 +0200 |
nipkow |
added "set" supression
|
changeset |
files
|
| Sun, 06 May 2007 13:33:01 +0200 |
nipkow |
added test about "set" supression
|
changeset |
files
|
| Fri, 04 May 2007 04:17:00 +0200 |
urbanc |
polished all proofs and made the theory "self-contained"
|
changeset |
files
|
| Thu, 03 May 2007 19:00:28 +0200 |
urbanc |
deleted some unnecessary type-annotations
|
changeset |
files
|
| Thu, 03 May 2007 17:54:36 +0200 |
urbanc |
tuned some of the proofs and added the lemma fresh_bool
|
changeset |
files
|
| Wed, 02 May 2007 21:00:06 +0200 |
nipkow |
tuned allpairs
|
changeset |
files
|
| Wed, 02 May 2007 01:42:23 +0200 |
urbanc |
tuned some proofs and changed variable names in some definitions of Nominal.thy
|
changeset |
files
|
| Mon, 30 Apr 2007 22:43:33 +0200 |
nipkow |
added allpairs
|
changeset |
files
|
| Mon, 30 Apr 2007 13:33:00 +0200 |
wenzelm |
removed obsolete get_sg;
|
changeset |
files
|
| Mon, 30 Apr 2007 13:32:58 +0200 |
wenzelm |
explicit treatment of legacy_features;
|
changeset |
files
|
| Mon, 30 Apr 2007 13:22:35 +0200 |
paulson |
Fixing bugs in the partial-typed and fully-typed translations
|
changeset |
files
|
| Mon, 30 Apr 2007 13:22:15 +0200 |
paulson |
Removal of dead code
|
changeset |
files
|
| Fri, 27 Apr 2007 18:50:27 +0200 |
urbanc |
tuned some proofs in CR and properly included CR_Takahashi
|
changeset |
files
|
| Fri, 27 Apr 2007 16:31:20 +0200 |
wenzelm |
removed obsolete induct/simp tactic;
|
changeset |
files
|
| Fri, 27 Apr 2007 14:21:23 +0200 |
urbanc |
alternative and much simpler proof for Church-Rosser of Beta-Reduction
|
changeset |
files
|
| Fri, 27 Apr 2007 05:53:37 +0200 |
kleing |
use correct email program for sunbroy2
|
changeset |
files
|
| Thu, 26 Apr 2007 16:39:31 +0200 |
wenzelm |
removed legacy ML files;
|
changeset |
files
|
| Thu, 26 Apr 2007 16:39:14 +0200 |
wenzelm |
eliminated unnamed infixes;
|
changeset |
files
|
| Thu, 26 Apr 2007 16:39:11 +0200 |
wenzelm |
added header;
|
changeset |
files
|
| Thu, 26 Apr 2007 16:39:10 +0200 |
wenzelm |
added header;
|
changeset |
files
|
| Thu, 26 Apr 2007 16:24:13 +0200 |
haftmann |
added
|
changeset |
files
|
| Thu, 26 Apr 2007 15:42:04 +0200 |
wenzelm |
removed lagacy ML files;
|
changeset |
files
|
| Thu, 26 Apr 2007 15:41:49 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Thu, 26 Apr 2007 14:25:37 +0200 |
wenzelm |
eliminated unnamed infixes;
|
changeset |
files
|
| Thu, 26 Apr 2007 14:24:14 +0200 |
wenzelm |
renamed some old names Theory.xxx to Sign.xxx;
|
changeset |
files
|
| Thu, 26 Apr 2007 14:24:13 +0200 |
wenzelm |
eliminated unnamed infixes;
|
changeset |
files
|
| Thu, 26 Apr 2007 14:24:12 +0200 |
wenzelm |
added header;
|
changeset |
files
|
| Thu, 26 Apr 2007 14:24:08 +0200 |
wenzelm |
eliminated unnamed infixes, tuned syntax;
|
changeset |
files
|
| Thu, 26 Apr 2007 13:33:17 +0200 |
haftmann |
clarified naming policy
|
changeset |
files
|
| Thu, 26 Apr 2007 13:33:16 +0200 |
haftmann |
clarified semantics of merge
|
changeset |
files
|
| Thu, 26 Apr 2007 13:33:15 +0200 |
haftmann |
moved stuff to Char_nat.thy
|
changeset |
files
|
| Thu, 26 Apr 2007 13:33:12 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Thu, 26 Apr 2007 13:33:09 +0200 |
haftmann |
slightly tuned
|
changeset |
files
|
| Thu, 26 Apr 2007 13:33:07 +0200 |
haftmann |
replaced recdef by function
|
changeset |
files
|
| Thu, 26 Apr 2007 13:33:05 +0200 |
haftmann |
cleaned up code generator setup for int
|
changeset |
files
|
| Thu, 26 Apr 2007 13:33:04 +0200 |
haftmann |
added lemmatas
|
changeset |
files
|
| Thu, 26 Apr 2007 13:32:59 +0200 |
haftmann |
moved code generation pretty integers and characters to separate theories
|
changeset |
files
|
| Thu, 26 Apr 2007 13:32:55 +0200 |
haftmann |
updated doc
|
changeset |
files
|
| Thu, 26 Apr 2007 12:00:12 +0200 |
wenzelm |
mk_const_def: Sign.intern_term (legacy);
|
changeset |
files
|
| Thu, 26 Apr 2007 12:00:05 +0200 |
wenzelm |
renamed some old names Theory.xxx to Sign.xxx;
|
changeset |
files
|
| Thu, 26 Apr 2007 12:00:01 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Wed, 25 Apr 2007 21:29:14 +0200 |
narboux |
add the lemma supp_eqvt and put the right attribute
|
changeset |
files
|
| Wed, 25 Apr 2007 17:50:48 +0200 |
nipkow |
new lemma splice_length
|
changeset |
files
|
| Wed, 25 Apr 2007 15:38:56 +0200 |
narboux |
fix sml compilation
|
changeset |
files
|
| Wed, 25 Apr 2007 15:26:01 +0200 |
berghofe |
Moved function params_of to inductive_package.ML.
|
changeset |
files
|
| Wed, 25 Apr 2007 15:25:22 +0200 |
berghofe |
Moved functions infer_intro_vars, arities_of, params_of, and
|
changeset |
files
|
| Wed, 25 Apr 2007 15:24:15 +0200 |
berghofe |
Added functions arities_of, params_of, partition_rules, and
|
changeset |
files
|
| Wed, 25 Apr 2007 15:22:57 +0200 |
berghofe |
eqvt_tac now instantiates introduction rules before applying them.
|
changeset |
files
|
| Tue, 24 Apr 2007 18:06:04 +0200 |
narboux |
update fresh_fun_simp for debugging purposes
|
changeset |
files
|
| Tue, 24 Apr 2007 17:16:55 +0200 |
narboux |
fixes last commit
|
changeset |
files
|
| Tue, 24 Apr 2007 16:44:11 +0200 |
narboux |
add two lemmas dealing with freshness on permutations.
|
changeset |
files
|
| Tue, 24 Apr 2007 15:19:33 +0200 |
berghofe |
Added datatype_case.ML and nominal_fresh_fun.ML.
|
changeset |
files
|
| Tue, 24 Apr 2007 15:18:42 +0200 |
berghofe |
Added datatype_case.
|
changeset |
files
|
| Tue, 24 Apr 2007 15:18:09 +0200 |
berghofe |
Added intro / elim rules for prod_case.
|
changeset |
files
|
| Tue, 24 Apr 2007 15:17:22 +0200 |
berghofe |
sum_case is now authentic.
|
changeset |
files
|
| Tue, 24 Apr 2007 15:15:52 +0200 |
berghofe |
Adapted to new parse translation for case expressions.
|
changeset |
files
|
| Tue, 24 Apr 2007 15:14:31 +0200 |
berghofe |
Parse / print translations for nested case expressions, taken
|
changeset |
files
|
| Tue, 24 Apr 2007 15:13:19 +0200 |
berghofe |
Streamlined datatype_codegen function using new datatype_of_case
|
changeset |
files
|
| Tue, 24 Apr 2007 15:11:07 +0200 |
berghofe |
- Moved parse / print translations for case to datatype_case.ML
|
changeset |
files
|
| Tue, 24 Apr 2007 15:07:27 +0200 |
berghofe |
case constants are now authentic.
|
changeset |
files
|
| Tue, 24 Apr 2007 14:02:16 +0200 |
narboux |
oups : wrong commit
|
changeset |
files
|
| Tue, 24 Apr 2007 14:01:23 +0200 |
narboux |
adds op in front of an infix to fix SML compilation
|
changeset |
files
|
| Mon, 23 Apr 2007 20:44:12 +0200 |
wenzelm |
sane version of read_termTs (proper freeze);
|
changeset |
files
|
| Mon, 23 Apr 2007 20:44:11 +0200 |
wenzelm |
read_instantiations: proper type-inference with fixed variables, infer parameter types as well;
|
changeset |
files
|
| Mon, 23 Apr 2007 20:44:10 +0200 |
wenzelm |
added paramify_vars;
|
changeset |
files
|
| Mon, 23 Apr 2007 20:44:09 +0200 |
wenzelm |
def_simproc(_i): proper ProofContext.read/cert_terms;
|
changeset |
files
|
| Mon, 23 Apr 2007 20:44:08 +0200 |
wenzelm |
simplified ProofContext.read_termTs;
|
changeset |
files
|
| Mon, 23 Apr 2007 18:38:42 +0200 |
urbanc |
simplified the proof of pt_set_eqvt (as suggested by Randy Pollack)
|
changeset |
files
|
| Mon, 23 Apr 2007 16:38:40 +0200 |
haftmann |
initial commit
|
changeset |
files
|
| Sat, 21 Apr 2007 19:32:32 +0200 |
huffman |
faster proof of wf_eq_minimal
|
changeset |
files
|
| Sat, 21 Apr 2007 11:07:45 +0200 |
wenzelm |
export get_sort (belongs to Syntax module);
|
changeset |
files
|
| Sat, 21 Apr 2007 11:07:44 +0200 |
wenzelm |
TypeExt.decode_term;
|
changeset |
files
|
| Sat, 21 Apr 2007 11:07:42 +0200 |
wenzelm |
added decode_term (belongs to Syntax module);
|
changeset |
files
|
| Sat, 21 Apr 2007 01:34:15 +0200 |
urbanc |
tuned the setup of fresh_fun
|
changeset |
files
|
| Fri, 20 Apr 2007 17:58:27 +0200 |
haftmann |
defs are added to code data
|
changeset |
files
|
| Fri, 20 Apr 2007 17:58:26 +0200 |
haftmann |
repaired value restriction problem
|
changeset |
files
|
| Fri, 20 Apr 2007 17:58:25 +0200 |
haftmann |
reverted to classical syntax for K_record
|
changeset |
files
|
| Fri, 20 Apr 2007 17:58:24 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Fri, 20 Apr 2007 16:55:38 +0200 |
ballarin |
Interpretation equations applied to attributes
|
changeset |
files
|
| Fri, 20 Apr 2007 16:54:57 +0200 |
ballarin |
Interpretation equations applied to attributes;
|
changeset |
files
|
| Fri, 20 Apr 2007 16:11:17 +0200 |
berghofe |
Modified eqvt_tac to avoid failure due to introduction rules
|
changeset |
files
|
| Fri, 20 Apr 2007 15:13:06 +0200 |
haftmann |
clarifed
|
changeset |
files
|
| Fri, 20 Apr 2007 14:30:35 +0200 |
narboux |
modify fresh_fun_simp to ease debugging
|
changeset |
files
|
| Fri, 20 Apr 2007 13:30:51 +0200 |
haftmann |
updated code generator
|
changeset |
files
|
| Fri, 20 Apr 2007 13:11:47 +0200 |
haftmann |
updated
|
changeset |
files
|
| Fri, 20 Apr 2007 11:21:53 +0200 |
haftmann |
adds extracted program to code theorem table
|
changeset |
files
|
| Fri, 20 Apr 2007 11:21:52 +0200 |
haftmann |
unfold attribute now also accepts HOL equations
|
changeset |
files
|
| Fri, 20 Apr 2007 11:21:50 +0200 |
haftmann |
added more stuff
|
changeset |
files
|
| Fri, 20 Apr 2007 11:21:49 +0200 |
haftmann |
add definitions explicitly to code generator table
|
changeset |
files
|
| Fri, 20 Apr 2007 11:21:48 +0200 |
haftmann |
cleared dead code
|
changeset |
files
|
| Fri, 20 Apr 2007 11:21:47 +0200 |
haftmann |
moved axclass module closer to core system
|
changeset |
files
|
| Fri, 20 Apr 2007 11:21:42 +0200 |
haftmann |
Isar definitions are now added explicitly to code theorem table
|
changeset |
files
|
| Fri, 20 Apr 2007 11:21:41 +0200 |
haftmann |
improved case unfolding
|
changeset |
files
|
| Fri, 20 Apr 2007 11:21:40 +0200 |
haftmann |
switched from recdef to function package; constants add, mul, pow now curried; infix syntax for algebraic operations.
|
changeset |
files
|
| Fri, 20 Apr 2007 11:21:39 +0200 |
haftmann |
tuned syntax: K_record is now an authentic constant
|
changeset |
files
|
| Fri, 20 Apr 2007 11:21:38 +0200 |
haftmann |
tuned: now using function package
|
changeset |
files
|
| Fri, 20 Apr 2007 11:21:37 +0200 |
haftmann |
transfer_tac accepts also HOL equations as theorems
|
changeset |
files
|
| Fri, 20 Apr 2007 11:21:36 +0200 |
haftmann |
shifted min/max to class order
|
changeset |
files
|
| Fri, 20 Apr 2007 11:21:35 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Fri, 20 Apr 2007 11:21:34 +0200 |
haftmann |
added class tutorial
|
changeset |
files
|
| Fri, 20 Apr 2007 11:21:33 +0200 |
haftmann |
code generator changes
|
changeset |
files
|
| Fri, 20 Apr 2007 10:09:32 +0200 |
krauss |
generate page labels
|
changeset |
files
|
| Fri, 20 Apr 2007 10:06:11 +0200 |
krauss |
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
|
changeset |
files
|
| Fri, 20 Apr 2007 00:28:07 +0200 |
urbanc |
declared lemmas true_eqvt and false_eqvt to be equivariant (suggested by samth at ccs.neu.edu)
|
changeset |
files
|
| Thu, 19 Apr 2007 18:23:11 +0200 |
paulson |
trying to make single-step proofs work better, especially if they contain
|
changeset |
files
|
| Thu, 19 Apr 2007 16:38:59 +0200 |
berghofe |
nominal_inductive no longer proves equivariance.
|
changeset |
files
|
| Thu, 19 Apr 2007 16:27:53 +0200 |
narboux |
add a tactic to generate fresh names
|
changeset |
files
|
| Wed, 18 Apr 2007 21:30:14 +0200 |
wenzelm |
simplified ProofContext.infer_types(_pats);
|
changeset |
files
|
| Wed, 18 Apr 2007 16:23:31 +0200 |
dixon |
Improved comments.
|
changeset |
files
|
| Wed, 18 Apr 2007 11:47:08 +0200 |
krauss |
proper header, added regression tests
|
changeset |
files
|
| Wed, 18 Apr 2007 11:37:43 +0200 |
krauss |
added temporary hack to avoid schematic goals in "termination".
|
changeset |
files
|
| Wed, 18 Apr 2007 11:14:09 +0200 |
paulson |
Fixes for proof reconstruction, especially involving abstractions and definitions
|
changeset |
files
|
| Tue, 17 Apr 2007 21:06:59 +0200 |
wenzelm |
export is_dummy_pattern;
|
changeset |
files
|
| Tue, 17 Apr 2007 03:13:38 +0200 |
huffman |
lemma isCont_inv_fun is same as isCont_inverse_function
|
changeset |
files
|
| Tue, 17 Apr 2007 00:55:00 +0200 |
huffman |
moved root and sqrt lemmas from Transcendental.thy to NthRoot.thy
|
changeset |
files
|
| Tue, 17 Apr 2007 00:37:14 +0200 |
huffman |
remove use of pos_boundedE
|
changeset |
files
|
| Tue, 17 Apr 2007 00:33:49 +0200 |
huffman |
lemma geometric_sum no longer needs class division_by_zero
|
changeset |
files
|
| Tue, 17 Apr 2007 00:30:44 +0200 |
wenzelm |
tuned proofs;
|
changeset |
files
|
| Mon, 16 Apr 2007 16:11:03 +0200 |
haftmann |
canonical merge operations
|
changeset |
files
|
| Mon, 16 Apr 2007 12:16:11 +0200 |
wenzelm |
added print_indexname;
|
changeset |
files
|
| Mon, 16 Apr 2007 07:32:23 +0200 |
urbanc |
improved the equivariance lemmas for the quantifiers; had to export the lemma eqvt_force_add and eqvt_force_del in the thmdecls
|
changeset |
files
|
| Mon, 16 Apr 2007 06:45:22 +0200 |
urbanc |
added a more usuable lemma for dealing with fresh_fun
|
changeset |
files
|
| Mon, 16 Apr 2007 04:02:15 +0200 |
huffman |
generalized type of lemma geometric_sum
|
changeset |
files
|
| Sun, 15 Apr 2007 23:25:55 +0200 |
wenzelm |
replaced read_term_legacy by read_prop_legacy;
|
changeset |
files
|
| Sun, 15 Apr 2007 23:25:54 +0200 |
wenzelm |
removed obsolete redeclare_skolems;
|
changeset |
files
|
| Sun, 15 Apr 2007 23:25:52 +0200 |
wenzelm |
read prop as prop, not term;
|
changeset |
files
|
| Sun, 15 Apr 2007 23:25:50 +0200 |
wenzelm |
removed obsolete TypeInfer.logicT -- use dummyT;
|
changeset |
files
|
| Sun, 15 Apr 2007 23:25:49 +0200 |
wenzelm |
avoid internal names;
|
changeset |
files
|
| Sun, 15 Apr 2007 14:32:55 +0200 |
wenzelm |
tuned;
|
changeset |
files
|
| Sun, 15 Apr 2007 14:32:07 +0200 |
wenzelm |
legacy_infer_term/prop -- including intern_term;
|
changeset |
files
|
| Sun, 15 Apr 2007 14:32:05 +0200 |
wenzelm |
Thm.plain_prop_of;
|
changeset |
files
|
| Sun, 15 Apr 2007 14:32:04 +0200 |
wenzelm |
added decode_types (from type_infer.ML);
|
changeset |
files
|
| Sun, 15 Apr 2007 14:32:03 +0200 |
wenzelm |
added read_term;
|
changeset |
files
|
| Sun, 15 Apr 2007 14:32:02 +0200 |
wenzelm |
added mixfixT (from type_infer.ML);
|
changeset |
files
|
| Sun, 15 Apr 2007 14:32:01 +0200 |
wenzelm |
proper interface infer_types(_pat);
|
changeset |
files
|
| Sun, 15 Apr 2007 14:32:00 +0200 |
wenzelm |
Thm.fold_terms;
|
changeset |
files
|
| Sun, 15 Apr 2007 14:31:59 +0200 |
wenzelm |
removed unused Output.panic hook -- internal to PG wrapper;
|
changeset |
files
|
| Sun, 15 Apr 2007 14:31:57 +0200 |
wenzelm |
moved get_sort to sign.ML;
|
changeset |
files
|
| Sun, 15 Apr 2007 14:31:56 +0200 |
wenzelm |
removed obsolete inferT_axm;
|
changeset |
files
|
| Sun, 15 Apr 2007 14:31:54 +0200 |
wenzelm |
removed obsolete infer_types(_simult);
|
changeset |
files
|
| Sun, 15 Apr 2007 14:31:53 +0200 |
wenzelm |
moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
|
changeset |
files
|
| Sun, 15 Apr 2007 14:31:52 +0200 |
wenzelm |
load type_infer.ML early;
|
changeset |
files
|
| Sun, 15 Apr 2007 14:31:51 +0200 |
wenzelm |
adapted decode_type;
|
changeset |
files
|
| Sun, 15 Apr 2007 14:31:49 +0200 |
wenzelm |
proper ProofContext.infer_types;
|
changeset |
files
|
| Sun, 15 Apr 2007 14:31:47 +0200 |
wenzelm |
Thm.fold_terms;
|
changeset |
files
|
| Sun, 15 Apr 2007 14:31:44 +0200 |
wenzelm |
replaced axioms/finalconsts by proper axiomatization;
|
changeset |
files
|
| Sat, 14 Apr 2007 23:56:36 +0200 |
wenzelm |
simplified read_axm;
|
changeset |
files
|
| Sat, 14 Apr 2007 17:38:30 +0200 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Sat, 14 Apr 2007 17:36:19 +0200 |
wenzelm |
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
|
changeset |
files
|
| Sat, 14 Apr 2007 17:36:18 +0200 |
wenzelm |
removed redundant string_of_vname (see term.ML);
|
changeset |
files
|
| Sat, 14 Apr 2007 17:36:17 +0200 |
wenzelm |
removed obsolete read_ctyp, read_def_cterm;
|
changeset |
files
|
| Sat, 14 Apr 2007 17:36:16 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sat, 14 Apr 2007 17:36:14 +0200 |
wenzelm |
read_typ_XXX: no sorts;
|
changeset |
files
|
| Sat, 14 Apr 2007 17:36:10 +0200 |
wenzelm |
added read_def_cterms, read_cterm (from thm.ML);
|
changeset |
files
|
| Sat, 14 Apr 2007 17:36:09 +0200 |
wenzelm |
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
|
changeset |
files
|
| Sat, 14 Apr 2007 17:36:07 +0200 |
wenzelm |
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
|
changeset |
files
|
| Sat, 14 Apr 2007 17:36:06 +0200 |
wenzelm |
removed Pure/Syntax/ROOT.ML;
|
changeset |
files
|
| Sat, 14 Apr 2007 17:36:05 +0200 |
wenzelm |
Term.string_of_vname;
|
changeset |
files
|
| Sat, 14 Apr 2007 17:36:03 +0200 |
wenzelm |
Theory.inferT_axm;
|
changeset |
files
|
| Sat, 14 Apr 2007 17:36:01 +0200 |
wenzelm |
do not enable Toplevel.debug globally;
|
changeset |
files
|
| Sat, 14 Apr 2007 17:35:52 +0200 |
wenzelm |
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
|
changeset |
files
|
| Sat, 14 Apr 2007 11:05:12 +0200 |
haftmann |
canonical merge operations
|
changeset |
files
|
| Sat, 14 Apr 2007 00:46:23 +0200 |
wenzelm |
declarations: apply target_morphism;
|
changeset |
files
|
| Sat, 14 Apr 2007 00:46:22 +0200 |
wenzelm |
inst(T)_morphism: avoid reference to static theory value;
|
changeset |
files
|
| Sat, 14 Apr 2007 00:46:21 +0200 |
wenzelm |
tuned signature;
|
changeset |
files
|
| Sat, 14 Apr 2007 00:46:20 +0200 |
wenzelm |
added Morphism.transform/form (generic non-sense);
|
changeset |
files
|
| Sat, 14 Apr 2007 00:46:20 +0200 |
wenzelm |
Morphism.transform/form;
|
changeset |
files
|
| Sat, 14 Apr 2007 00:46:18 +0200 |
wenzelm |
data declaration: removed obsolete target_morphism (still required for local data!?);
|
changeset |
files
|
| Sat, 14 Apr 2007 00:46:17 +0200 |
wenzelm |
data declaration: removed obsolete target_morphism;
|
changeset |
files
|
| Fri, 13 Apr 2007 21:38:29 +0200 |
wenzelm |
added eval_antiquotes_fn (tmp);
|
changeset |
files
|
| Fri, 13 Apr 2007 21:26:35 +0200 |
wenzelm |
tuned document (headers, sections, spacing);
|
changeset |
files
|
| Fri, 13 Apr 2007 21:26:34 +0200 |
wenzelm |
do translation: CONST;
|
changeset |
files
|
| Fri, 13 Apr 2007 20:23:18 +0200 |
wenzelm |
eval_antiquotes: proper parentheses for projection;
|
changeset |
files
|
| Fri, 13 Apr 2007 16:40:16 +0200 |
haftmann |
canonical merge operations
|
changeset |
files
|
| Fri, 13 Apr 2007 15:43:25 +0200 |
berghofe |
Removed erroneous application of rev in get_clauses that caused
|
changeset |
files
|
| Fri, 13 Apr 2007 12:30:47 +0200 |
krauss |
more robust proof
|
changeset |
files
|
| Fri, 13 Apr 2007 10:02:30 +0200 |
ballarin |
Experimental code for the interpretation of definitions.
|
changeset |
files
|
| Fri, 13 Apr 2007 10:01:43 +0200 |
ballarin |
Experimental interpretation code for definitions.
|
changeset |
files
|
| Fri, 13 Apr 2007 10:00:04 +0200 |
ballarin |
New file for locale regression tests.
|
changeset |
files
|
| Fri, 13 Apr 2007 09:23:35 +0200 |
narboux |
debug versions of finite_guess and fresh_guess do not fail if they can not solve the goal
|
changeset |
files
|
| Fri, 13 Apr 2007 01:06:12 +0200 |
huffman |
minimize imports
|
changeset |
files
|
| Fri, 13 Apr 2007 00:48:12 +0200 |
huffman |
new simp rule exp_ln; new standard proof of DERIV_exp_ln_one; changed imports
|
changeset |
files
|
| Fri, 13 Apr 2007 00:07:52 +0200 |
huffman |
moved nonstandard derivative stuff from Deriv.thy into new file HDeriv.thy
|
changeset |
files
|
| Thu, 12 Apr 2007 23:06:27 +0200 |
wenzelm |
added proj_value_antiq;
|
changeset |
files
|
| Thu, 12 Apr 2007 23:06:25 +0200 |
wenzelm |
absdummy: use internal name uu to avoid renaming of popular names;
|
changeset |
files
|
| Thu, 12 Apr 2007 15:46:12 +0200 |
urbanc |
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
|
changeset |
files
|
| Thu, 12 Apr 2007 15:35:29 +0200 |
wenzelm |
updated;
|
changeset |
files
|
| Thu, 12 Apr 2007 15:01:13 +0200 |
wenzelm |
output_basic: added isaantiq markup (only inside verbatim tokens);
|
changeset |
files
|
| Thu, 12 Apr 2007 15:01:11 +0200 |
wenzelm |
newenvironment{isaantiq};
|
changeset |
files
|
| Thu, 12 Apr 2007 13:58:47 +0200 |
paulson |
Zero variable indexes in clauses
|
changeset |
files
|
| Thu, 12 Apr 2007 13:58:02 +0200 |
paulson |
Improved treatment of classrel/arity clauses
|
changeset |
files
|
| Thu, 12 Apr 2007 13:57:27 +0200 |
paulson |
Fixed the treatment of TVars in conjecture clauses (they are deleted, not frozen)
|
changeset |
files
|
| Thu, 12 Apr 2007 13:56:40 +0200 |
paulson |
Improved and simplified the treatment of classrel/arity clauses
|
changeset |
files
|
| Thu, 12 Apr 2007 12:26:19 +0200 |
haftmann |
canonical merge operations
|
changeset |
files
|
| Thu, 12 Apr 2007 03:37:30 +0200 |
huffman |
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
|
changeset |
files
|
| Thu, 12 Apr 2007 02:59:44 +0200 |
kleing |
run annomaly from makedist
|
changeset |
files
|
| Thu, 12 Apr 2007 02:44:33 +0200 |
isatest |
set special ISABELLE_USER_HOME as in other isatest settings
|
changeset |
files
|
| Thu, 12 Apr 2007 02:42:58 +0200 |
kleing |
isatest version of annomaly script. to be run from istatest-makedist.
|
changeset |
files
|
| Thu, 12 Apr 2007 01:53:02 +0200 |
huffman |
new standard proof of lemma LIM_inverse
|
changeset |
files
|
| Wed, 11 Apr 2007 19:42:43 +0200 |
huffman |
new class syntax for scaleR and norm classes
|
changeset |
files
|
| Wed, 11 Apr 2007 09:40:29 +0200 |
krauss |
removed debugging code
|
changeset |
files
|
| Wed, 11 Apr 2007 08:28:15 +0200 |
haftmann |
canonical merge operations
|
changeset |
files
|
| Wed, 11 Apr 2007 08:28:14 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Wed, 11 Apr 2007 08:28:13 +0200 |
haftmann |
dropped legacy ML bindings
|
changeset |
files
|
| Wed, 11 Apr 2007 04:13:06 +0200 |
huffman |
moved nonstandard stuff from SEQ.thy into new file HSEQ.thy
|
changeset |
files
|
| Wed, 11 Apr 2007 03:54:53 +0200 |
huffman |
move lemma real_of_nat_inverse_le_iff from NSA.thy to NthRoot.thy
|
changeset |
files
|
| Wed, 11 Apr 2007 02:19:06 +0200 |
huffman |
new standard proof of convergent = Cauchy
|
changeset |
files
|
| Tue, 10 Apr 2007 22:02:43 +0200 |
huffman |
new standard proof of LIMSEQ_realpow_zero
|
changeset |
files
|
| Tue, 10 Apr 2007 22:01:19 +0200 |
huffman |
new LIM/isCont lemmas for abs, of_real, and power
|
changeset |
files
|
| Tue, 10 Apr 2007 21:52:38 +0200 |
krauss |
some restructuring
|
changeset |
files
|
| Tue, 10 Apr 2007 21:51:08 +0200 |
huffman |
interpretation bounded_linear_of_real
|
changeset |
files
|
| Tue, 10 Apr 2007 21:50:08 +0200 |
huffman |
removed unnecessary premise from power_le_imp_le_base
|
changeset |
files
|
| Tue, 10 Apr 2007 18:09:58 +0200 |
krauss |
proper handling of morphisms
|
changeset |
files
|
| Tue, 10 Apr 2007 14:11:01 +0200 |
krauss |
Moving "FunDef" up in the HOL development graph, since it is independent from "Recdef" and "Datatype" now.
|
changeset |
files
|
| Tue, 10 Apr 2007 11:55:23 +0200 |
wenzelm |
inline_antiq: no longer forces ML_Syntax.atomic;
|
changeset |
files
|
| Tue, 10 Apr 2007 11:12:55 +0200 |
krauss |
removed dead code
|
changeset |
files
|
| Tue, 10 Apr 2007 11:12:42 +0200 |
krauss |
tuned
|
changeset |
files
|
| Tue, 10 Apr 2007 08:19:20 +0200 |
krauss |
added example for definitions in local contexts
|
changeset |
files
|
| Tue, 10 Apr 2007 08:09:28 +0200 |
krauss |
removed obsolete workaround
|
changeset |
files
|
| Mon, 09 Apr 2007 21:28:24 +0200 |
huffman |
generalized type of lemma setsum_product
|
changeset |
files
|
| Mon, 09 Apr 2007 04:51:28 +0200 |
huffman |
new standard proofs of some LIMSEQ lemmas
|
changeset |
files
|
| Sun, 08 Apr 2007 18:35:19 +0200 |
huffman |
rearranged sections
|
changeset |
files
|
| Sun, 08 Apr 2007 17:54:52 +0200 |
huffman |
remove redundant lemmas
|
changeset |
files
|
| Sat, 07 Apr 2007 18:54:30 +0200 |
krauss |
removed obsolete workarounds
|
changeset |
files
|
| Sat, 07 Apr 2007 12:40:32 +0200 |
urbanc |
deleted remaining instances of swap_simp_a and swap_simp_b (obsolete now)
|
changeset |
files
|
| Sat, 07 Apr 2007 11:36:35 +0200 |
urbanc |
tuned slightly the previous commit
|
changeset |
files
|
| Sat, 07 Apr 2007 11:05:25 +0200 |
narboux |
perm_simp can now simplify using the rules (a,b) o a = b and (a,b) o b = a
|
changeset |
files
|
| Fri, 06 Apr 2007 01:26:30 +0200 |
huffman |
add new standard proofs for limits of sequences
|
changeset |
files
|
| Thu, 05 Apr 2007 14:56:54 +0200 |
berghofe |
Replaced add_inductive_i by add_inductive_global.
|
changeset |
files
|
| Thu, 05 Apr 2007 14:56:10 +0200 |
berghofe |
- Tried to make name_of_thm more robust against changes of the
|
changeset |
files
|
| Thu, 05 Apr 2007 14:51:28 +0200 |
berghofe |
- Removed occurrences of ProofContext.export in add_ind_def that
|
changeset |
files
|
| Thu, 05 Apr 2007 00:30:32 +0200 |
wenzelm |
thy_deps: sort Context.thy_ord;
|
changeset |
files
|
| Thu, 05 Apr 2007 00:30:31 +0200 |
wenzelm |
added thy_ord -- order of creation;
|
changeset |
files
|
| Wed, 04 Apr 2007 23:29:42 +0200 |
wenzelm |
simplified thy_deps using Theory.ancestors_of (in order of creation);
|
changeset |
files
|
| Wed, 04 Apr 2007 23:29:41 +0200 |
wenzelm |
renamed Variable.importT to importT_thms;
|
changeset |
files
|
| Wed, 04 Apr 2007 23:29:40 +0200 |
wenzelm |
removed unused dep_graph;
|
changeset |
files
|
| Wed, 04 Apr 2007 23:29:39 +0200 |
wenzelm |
theory: maintain ancestors in order of creation;
|
changeset |
files
|
| Wed, 04 Apr 2007 23:29:38 +0200 |
wenzelm |
rep_thm/cterm/ctyp: removed obsolete sign field;
|
changeset |
files
|
| Wed, 04 Apr 2007 23:29:37 +0200 |
wenzelm |
rebind HOL.refl as refl (hidden by widen.refl);
|
changeset |
files
|
| Wed, 04 Apr 2007 23:29:33 +0200 |
wenzelm |
rep_thm/cterm/ctyp: removed obsolete sign field;
|
changeset |
files
|
| Wed, 04 Apr 2007 20:22:32 +0200 |
narboux |
make fresh_guess fail if it does not solve the subgoal
|
changeset |
files
|
| Wed, 04 Apr 2007 19:56:25 +0200 |
narboux |
add a few details in the Fst and Snd cases of unicity proof
|
changeset |
files
|
| Wed, 04 Apr 2007 18:05:05 +0200 |
paulson |
find_first is just an alias
|
changeset |
files
|
| Wed, 04 Apr 2007 00:13:13 +0200 |
wenzelm |
added print_mode (generic non-sense);
|
changeset |
files
|
| Wed, 04 Apr 2007 00:11:26 +0200 |
wenzelm |
improved exception CTERM;
|
changeset |
files
|
| Wed, 04 Apr 2007 00:11:23 +0200 |
wenzelm |
removed unused info channel;
|
changeset |
files
|
| Wed, 04 Apr 2007 00:11:22 +0200 |
wenzelm |
added print_mode;
|
changeset |
files
|
| Wed, 04 Apr 2007 00:11:21 +0200 |
wenzelm |
removed unused info channel;
|
changeset |
files
|
| Wed, 04 Apr 2007 00:11:20 +0200 |
wenzelm |
renamed Output.has_mode to print_mode_active;
|
changeset |
files
|
| Wed, 04 Apr 2007 00:11:18 +0200 |
wenzelm |
tuned comment;
|
changeset |
files
|
| Wed, 04 Apr 2007 00:11:17 +0200 |
wenzelm |
cleaned-up Output functions;
|
changeset |
files
|
| Wed, 04 Apr 2007 00:11:16 +0200 |
wenzelm |
improved exception CTERM;
|
changeset |
files
|
| Wed, 04 Apr 2007 00:11:14 +0200 |
wenzelm |
added scanwords from library.ML (for obsolete rename_tac);
|
changeset |
files
|
| Wed, 04 Apr 2007 00:11:13 +0200 |
wenzelm |
removed obsolete scanwords (see obsolete tactic.ML:rename_tac for its only use);
|
changeset |
files
|
| Wed, 04 Apr 2007 00:11:12 +0200 |
wenzelm |
removed dead code;
|
changeset |
files
|
| Wed, 04 Apr 2007 00:11:10 +0200 |
wenzelm |
cleaned-up Output functions;
|
changeset |
files
|
| Wed, 04 Apr 2007 00:11:08 +0200 |
wenzelm |
eliminated obsolete rename_tac;
|
changeset |
files
|
| Wed, 04 Apr 2007 00:11:03 +0200 |
wenzelm |
removed obsolete sign_of/sign_of_thm;
|
changeset |
files
|
| Wed, 04 Apr 2007 00:10:59 +0200 |
wenzelm |
ML antiquotes;
|
changeset |
files
|
| Tue, 03 Apr 2007 19:31:48 +0200 |
wenzelm |
tuned comments;
|
changeset |
files
|
| Tue, 03 Apr 2007 19:24:22 +0200 |
wenzelm |
fixed chr/explode;
|
changeset |
files
|
| Tue, 03 Apr 2007 19:24:21 +0200 |
wenzelm |
avoid overloaded integer constants (accomodate Alice);
|
changeset |
files
|
| Tue, 03 Apr 2007 19:24:19 +0200 |
wenzelm |
avoid clash with Alice keywords;
|
changeset |
files
|
| Tue, 03 Apr 2007 19:24:18 +0200 |
wenzelm |
signature: eqtype to accomodate Alice;
|
changeset |
files
|
| Tue, 03 Apr 2007 19:24:17 +0200 |
wenzelm |
renamed comp to compose (avoid clash with Alice keywords);
|
changeset |
files
|
| Tue, 03 Apr 2007 19:24:16 +0200 |
wenzelm |
renamed of_sort_derivation record fields (avoid clash with Alice keywords);
|
changeset |
files
|
| Tue, 03 Apr 2007 19:24:15 +0200 |
wenzelm |
added ML-Systems/alice.ML;
|
changeset |
files
|
| Tue, 03 Apr 2007 19:24:13 +0200 |
wenzelm |
renamed Variable.import to import_thms (avoid clash with Alice keywords);
|
changeset |
files
|
| Tue, 03 Apr 2007 19:24:11 +0200 |
wenzelm |
removed assert/deny (avoid clash with Alice keywords and confusion due to strict evaluation);
|
changeset |
files
|
| Tue, 03 Apr 2007 19:24:10 +0200 |
wenzelm |
ranamed CodegenData.lazy to lazy_thms (avoid clash with Alice keywords);
|
changeset |
files
|
| Tue, 03 Apr 2007 17:05:52 +0200 |
narboux |
remove the lemma swap_fun which was not needed
|
changeset |
files
|
| Tue, 03 Apr 2007 16:20:34 +0200 |
narboux |
slighltly improved the proof of unicity
|
changeset |
files
|
| Tue, 03 Apr 2007 12:12:42 +0200 |
wenzelm |
Compatibility file for Alice 1.3 -- experimental!
|
changeset |
files
|
| Mon, 02 Apr 2007 23:24:52 +0200 |
narboux |
rename bij and fresh into bijs and freshs and lookup for eqvts lemma using the ml value instead of the name
|
changeset |
files
|
| Mon, 02 Apr 2007 11:31:08 +0200 |
paulson |
optimizing the null instantiation case
|
changeset |
files
|
| Mon, 02 Apr 2007 11:30:44 +0200 |
paulson |
now exports distinct_subgoal_tac (needed by MetisAPI)
|
changeset |
files
|
| Mon, 02 Apr 2007 11:29:44 +0200 |
paulson |
exception handling
|
changeset |
files
|
| Sun, 01 Apr 2007 14:28:48 +0200 |
haftmann |
added reserved words mod, div for SML
|
changeset |
files
|
| Sat, 31 Mar 2007 15:13:52 +0200 |
urbanc |
added pt_bij' to the collection perm_swap and also added abs_perm to the collection of equivariance lemmas
|
changeset |
files
|
| Sat, 31 Mar 2007 12:40:55 +0200 |
berghofe |
Fixed bug in dest_prem: premises of the form "p x_1 ... x_n"
|
changeset |
files
|
| Sat, 31 Mar 2007 08:22:14 +0200 |
haftmann |
fixed typo
|
changeset |
files
|
| Fri, 30 Mar 2007 16:19:03 +0200 |
haftmann |
simplified constant representation in code generator
|
changeset |
files
|
| Fri, 30 Mar 2007 16:19:02 +0200 |
haftmann |
tuned
|
changeset |
files
|
| Fri, 30 Mar 2007 16:19:01 +0200 |
haftmann |
equality on strings
|
changeset |
files
|
| Fri, 30 Mar 2007 16:19:00 +0200 |
haftmann |
paraphrasing equality
|
changeset |
files
|
| Fri, 30 Mar 2007 16:18:59 +0200 |
haftmann |
updated
|
changeset |
files
|
| Thu, 29 Mar 2007 14:21:47 +0200 |
haftmann |
improved character output for SML
|
changeset |
files
|
| Thu, 29 Mar 2007 14:21:45 +0200 |
haftmann |
dropped legacy ML bindings
|
changeset |
files
|
| Thu, 29 Mar 2007 11:59:54 +0200 |
paulson |
simplified some steps
|
changeset |
files
|
| Thu, 29 Mar 2007 11:12:39 +0200 |
paulson |
MESON tactical takes an additional argument: the clausification function.
|
changeset |
files
|
| Thu, 29 Mar 2007 11:12:03 +0200 |
paulson |
Now checks for types-only clause before outputting.
|
changeset |
files
|
| Wed, 28 Mar 2007 19:18:39 +0200 |
berghofe |
- Improved error messages in equivariance proof
|
changeset |
files
|
| Wed, 28 Mar 2007 19:17:40 +0200 |
berghofe |
Renamed induct(s)_weak to weak_induct(s) in order to unify
|
changeset |
files
|
| Wed, 28 Mar 2007 19:16:11 +0200 |
berghofe |
- Renamed <predicate>_eqvt to <predicate>.eqvt
|
changeset |
files
|
| Wed, 28 Mar 2007 18:25:23 +0200 |
urbanc |
the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvt-lemmas generated in nominal_inductive
|
changeset |
files
|
| Wed, 28 Mar 2007 17:27:44 +0200 |
urbanc |
adapted to new nominal_inductive
|
changeset |
files
|
| 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
|