wenzelm [Fri, 21 May 2004 21:27:42 +0200] rev 14792
added fold, product; removed transitive_closure;
wenzelm [Fri, 21 May 2004 21:27:10 +0200] rev 14791
adapted names of some sort ops;
wenzelm [Fri, 21 May 2004 21:26:19 +0200] rev 14790
major cleanup of tsig datastructures and extend/merge operations; fixes old bugs in classes/arities code; proper treatment of nonterminals and syntax-only types;
wenzelm [Fri, 21 May 2004 21:25:57 +0200] rev 14789
Type.strip_sorts;
wenzelm [Fri, 21 May 2004 21:25:34 +0200] rev 14788
incorporate type inference interface from type.ML;
wenzelm [Fri, 21 May 2004 21:24:22 +0200] rev 14787
adapted tsig interface;
wenzelm [Fri, 21 May 2004 21:23:37 +0200] rev 14786
moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);
wenzelm [Fri, 21 May 2004 21:23:12 +0200] rev 14785
test_classrel/arity improve error reporting; tuned;
wenzelm [Fri, 21 May 2004 21:22:42 +0200] rev 14784
xxx_typ_raw replace xxx_typ_no_norm forms; prevent duplicate consts declarations in merge; misc cleanup;
wenzelm [Fri, 21 May 2004 21:22:10 +0200] rev 14783
string_of_vname moved to term.ML;
wenzelm [Fri, 21 May 2004 21:21:51 +0200] rev 14782
incorporate sort ops from term.ML; use Graph.T; misc cleanup;
wenzelm [Fri, 21 May 2004 21:21:38 +0200] rev 14781
type.ML now before Syntax module;
wenzelm [Fri, 21 May 2004 21:21:12 +0200] rev 14780
xxx_typ_raw replace xxx_typ_no_norm forms;
wenzelm [Fri, 21 May 2004 21:20:38 +0200] rev 14779
'classrel' now allows multiple arguments;
wenzelm [Fri, 21 May 2004 21:20:14 +0200] rev 14778
Sign.certify_tyname;
wenzelm [Fri, 21 May 2004 21:19:47 +0200] rev 14777
TypeInfer.paramify_dummies, TypeInfer.param;
wenzelm [Fri, 21 May 2004 21:19:18 +0200] rev 14776
Args.local_typ_raw;
wenzelm [Fri, 21 May 2004 21:19:04 +0200] rev 14775
output_tym: removed duplicate clauses;
wenzelm [Fri, 21 May 2004 21:18:48 +0200] rev 14774
Graph.minimals;
wenzelm [Fri, 21 May 2004 21:18:35 +0200] rev 14773
adapted syntax to cope with lack of non-logical types;
wenzelm [Fri, 21 May 2004 21:18:14 +0200] rev 14772
Type.typ_instance;
wenzelm [Fri, 21 May 2004 21:17:37 +0200] rev 14771
load ML files only once;
wenzelm [Fri, 21 May 2004 21:16:51 +0200] rev 14770
removed duplicate thms;
wenzelm [Fri, 21 May 2004 21:15:45 +0200] rev 14769
Sign.typ_instance;
wenzelm [Fri, 21 May 2004 21:15:22 +0200] rev 14768
tuned message;
wenzelm [Fri, 21 May 2004 21:15:10 +0200] rev 14767
tuned document;
wenzelm [Fri, 21 May 2004 21:14:52 +0200] rev 14766
use plain SOME;
wenzelm [Fri, 21 May 2004 21:14:18 +0200] rev 14765
proper use of 'syntax';
paulson [Wed, 19 May 2004 11:41:58 +0200] rev 14764
auto update
paulson [Wed, 19 May 2004 11:31:26 +0200] rev 14763
has_consts now handles the @-operator
paulson [Wed, 19 May 2004 11:30:56 +0200] rev 14762
new bij_betw operator
paulson [Wed, 19 May 2004 11:30:18 +0200] rev 14761
more results about isomorphisms
paulson [Wed, 19 May 2004 11:29:47 +0200] rev 14760
conversion of Hilbert_Choice to Isar script
chaieb [Wed, 19 May 2004 11:24:54 +0200] rev 14759
the function list1 has been exported.
chaieb [Wed, 19 May 2004 11:23:59 +0200] rev 14758
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller.
the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.
chaieb [Wed, 19 May 2004 11:21:19 +0200] rev 14757
tactic call changed from TRYALL arith_tac to TRYALL simple_arith_tac preventing a call to presburger.
obua [Tue, 18 May 2004 11:45:50 +0200] rev 14756
modified abel_cancel.ML for polymorphic types
obua [Tue, 18 May 2004 10:02:50 +0200] rev 14755
simplification for abelian groups
obua [Tue, 18 May 2004 10:01:44 +0200] rev 14754
Modification / Installation of Provers/Arith/abel_cancel.ML for OrderedGroup.thy
webertj [Mon, 17 May 2004 14:05:06 +0200] rev 14753
Comments fixed
mehta [Mon, 17 May 2004 11:02:16 +0200] rev 14752
lemma disjoint_int_union removed - too special
ballarin [Fri, 14 May 2004 19:29:22 +0200] rev 14751
Change of theory hierarchy: Group is now based in Lattice.
paulson [Fri, 14 May 2004 16:54:13 +0200] rev 14750
tidied
paulson [Fri, 14 May 2004 16:53:15 +0200] rev 14749
new atomize theorem
paulson [Fri, 14 May 2004 16:52:53 +0200] rev 14748
removed a premise of card_inj_on_le
paulson [Fri, 14 May 2004 16:50:33 +0200] rev 14747
removal of locale coset
paulson [Fri, 14 May 2004 16:50:13 +0200] rev 14746
deleted redundant proof lines
paulson [Fri, 14 May 2004 16:49:42 +0200] rev 14745
new lemmas
paulson [Fri, 14 May 2004 16:49:12 +0200] rev 14744
clauses for ordinary resolution
paulson [Fri, 14 May 2004 16:48:37 +0200] rev 14743
conversion of theorems to atomic form
mehta [Thu, 13 May 2004 16:02:29 +0200] rev 14742
New simp rules added:
insert_disjoint
disjoint_insert
disjoint_int_union
paulson [Wed, 12 May 2004 10:40:41 +0200] rev 14741
simpilified and strengthened proofs
nipkow [Wed, 12 May 2004 10:00:56 +0200] rev 14740
fixed latex problems
nipkow [Wed, 12 May 2004 08:14:29 +0200] rev 14739
renamed `> to o_m
obua [Tue, 11 May 2004 20:11:08 +0200] rev 14738
changes made due to new Ring_and_Field theory
berghofe [Tue, 11 May 2004 14:00:02 +0200] rev 14737
Eta-expanded function scan_comment to make SmlNJ happy.
paulson [Tue, 11 May 2004 10:49:58 +0200] rev 14736
broken no longer includes TTP, and other minor changes
paulson [Tue, 11 May 2004 10:49:04 +0200] rev 14735
removal of prime characters
paulson [Tue, 11 May 2004 10:48:30 +0200] rev 14734
package needed for superscripts
paulson [Tue, 11 May 2004 10:48:00 +0200] rev 14733
conversion to clauses for ordinary resolution rather than ME