wenzelm [Thu, 16 Oct 1997 14:52:35 +0200] rev 3901
tuned;
wenzelm [Thu, 16 Oct 1997 14:48:10 +0200] rev 3900
removed begin;
added global section;
added global_names flag (tmp), default true;
wenzelm [Thu, 16 Oct 1997 14:46:55 +0200] rev 3899
fixed prep_ext;
nipkow [Thu, 16 Oct 1997 14:14:01 +0200] rev 3898
Simplified proof.
nipkow [Thu, 16 Oct 1997 14:12:58 +0200] rev 3897
Simplified proof because of better simplifier.
nipkow [Thu, 16 Oct 1997 14:12:15 +0200] rev 3896
Various new lemmas. Improved conversion of equations to rewrite rules:
(s=t becomes (s=t)==True if s=t loops).
wenzelm [Thu, 16 Oct 1997 14:00:20 +0200] rev 3895
added transfer: theory -> thm -> thm;
wenzelm [Thu, 16 Oct 1997 13:45:27 +0200] rev 3894
oops;
nipkow [Thu, 16 Oct 1997 13:45:16 +0200] rev 3893
The simplifier has been improved a little: equations s=t which used to be
rejected because of looping are now treated as (s=t) == True. The latter
translation must be done outside of Thm because it involves the object-logic
specific True. Therefore the simple loop test has been moved from Thm to
Logic.
wenzelm [Thu, 16 Oct 1997 13:43:42 +0200] rev 3892
fixed dependencies;
wenzelm [Thu, 16 Oct 1997 13:42:53 +0200] rev 3891
transfer thy Ord_nat;
wenzelm [Thu, 16 Oct 1997 13:42:29 +0200] rev 3890
sevaral goals restated in mono.thy;
wenzelm [Thu, 16 Oct 1997 13:39:20 +0200] rev 3889
moved rank_Inl, rank_Inr from Epsilon.ML to Univ.ML;
wenzelm [Thu, 16 Oct 1997 13:38:47 +0200] rev 3888
transfer InfDatatype.thy Limit_VfromE;
wenzelm [Thu, 16 Oct 1997 13:38:28 +0200] rev 3887
transfer CardinalArith.thy nat_into_Ord;
wenzelm [Thu, 16 Oct 1997 13:36:04 +0200] rev 3886
improved pretty_arity;
wenzelm [Thu, 16 Oct 1997 13:34:15 +0200] rev 3885
added merge_theories (new name arg);
wenzelm [Thu, 16 Oct 1997 13:33:17 +0200] rev 3884
fixed merge_theories;
wenzelm [Thu, 16 Oct 1997 13:28:04 +0200] rev 3883
revert to 1.3;
wenzelm [Thu, 16 Oct 1997 13:20:31 +0200] rev 3882
revert to 1.1;
nipkow [Thu, 16 Oct 1997 13:13:03 +0200] rev 3881
Added last, butlast, dropped ttl.
mueller [Thu, 16 Oct 1997 10:29:56 +0200] rev 3880
lala
paulson [Thu, 16 Oct 1997 10:22:37 +0200] rev 3879
Eta-expansion of function declarations, for value polymorphism
wenzelm [Wed, 15 Oct 1997 15:18:41 +0200] rev 3878
remove merge_theories;
merge_list: always prepares extend -- no longer supports aliasing merges;
wenzelm [Wed, 15 Oct 1997 15:17:32 +0200] rev 3877
make_draft replaced by prep_ext;
improved print_data;
merge now does trivial (absorptive) merges only;
added nontriv_merge;
wenzelm [Wed, 15 Oct 1997 15:15:22 +0200] rev 3876
tuned;
wenzelm [Wed, 15 Oct 1997 15:14:56 +0200] rev 3875
eliminated aliasing merge: now always extends;
wenzelm [Wed, 15 Oct 1997 15:13:43 +0200] rev 3874
tuned comment;
wenzelm [Wed, 15 Oct 1997 15:13:25 +0200] rev 3873
improved print_data;
wenzelm [Wed, 15 Oct 1997 15:12:59 +0200] rev 3872
tuned;
prepare ext;
wenzelm [Wed, 15 Oct 1997 11:43:27 +0200] rev 3871
slightly changed interfaces for oracles;
nipkow [Wed, 15 Oct 1997 11:27:55 +0200] rev 3870
Added ack to Mateja Jamnik.
wenzelm [Wed, 15 Oct 1997 11:16:48 +0200] rev 3869
tuned;
wenzelm [Tue, 14 Oct 1997 17:36:45 +0200] rev 3868
tuned;
wenzelm [Tue, 14 Oct 1997 17:36:22 +0200] rev 3867
added additional generic data;
wenzelm [Tue, 14 Oct 1997 17:35:56 +0200] rev 3866
Sign.print_data;
wenzelm [Tue, 14 Oct 1997 17:35:35 +0200] rev 3865
added init_data, get_data, put_data;
wenzelm [Tue, 14 Oct 1997 17:34:36 +0200] rev 3864
added data.ML;
wenzelm [Tue, 14 Oct 1997 17:34:21 +0200] rev 3863
Arbitrarily typed data.
paulson [Tue, 14 Oct 1997 17:23:01 +0200] rev 3862
Patch to avoid simplification of ~EX to ALL~
Also some better indentation
nipkow [Tue, 14 Oct 1997 13:59:12 +0200] rev 3861
Two lemmas are already in List.
nipkow [Tue, 14 Oct 1997 13:58:47 +0200] rev 3860
More lemmas, esp. ~Bex and ~Ball conversions.
nipkow [Tue, 14 Oct 1997 12:41:11 +0200] rev 3859
Added neagtion rules for Ball and Bex.
ZF/AC now fails to build. Larry to fix.
wenzelm [Tue, 14 Oct 1997 11:57:14 +0200] rev 3858
tuned;
wenzelm [Tue, 14 Oct 1997 11:30:35 +0200] rev 3857
browser info;
paulson [Tue, 14 Oct 1997 10:52:17 +0200] rev 3856
rearranged and added TLA
wenzelm [Mon, 13 Oct 1997 17:49:50 +0200] rev 3855
fixed extern;
added str_of_classrel, str_of_arity, str_of_arity;
wenzelm [Mon, 13 Oct 1997 17:49:08 +0200] rev 3854
uses Sign.str_of_classrel, Sign.str_of_arity, Sign.str_of_arity;
wenzelm [Mon, 13 Oct 1997 17:47:59 +0200] rev 3853
uses Sign.str_of_sort;
wenzelm [Mon, 13 Oct 1997 12:51:51 +0200] rev 3852
fixed dots;
wenzelm [Mon, 13 Oct 1997 12:48:42 +0200] rev 3851
print_goals: optional output of const types (set show_consts);
wenzelm [Mon, 13 Oct 1997 12:48:23 +0200] rev 3850
merge: drops path elements;
merz [Mon, 13 Oct 1997 11:00:06 +0200] rev 3849
Absolute URL's for documentation
wenzelm [Mon, 13 Oct 1997 10:31:21 +0200] rev 3848
non-transparent logo;
wenzelm [Mon, 13 Oct 1997 10:22:28 +0200] rev 3847
fixed dots;
wenzelm [Mon, 13 Oct 1997 10:14:52 +0200] rev 3846
hierachically structured name spaces;
berghofe [Sun, 12 Oct 1997 22:06:00 +0200] rev 3845
Changed logo.
berghofe [Sun, 12 Oct 1997 22:04:06 +0200] rev 3844
Added command for copying new logo.
wenzelm [Fri, 10 Oct 1997 19:13:58 +0200] rev 3843
fixed dots;
wenzelm [Fri, 10 Oct 1997 19:02:28 +0200] rev 3842
fixed dots;
wenzelm [Fri, 10 Oct 1997 18:37:49 +0200] rev 3841
fixed fixed dots;
wenzelm [Fri, 10 Oct 1997 18:23:31 +0200] rev 3840
fixed dots;
wenzelm [Fri, 10 Oct 1997 18:17:17 +0200] rev 3839
fixed dots;
wenzelm [Fri, 10 Oct 1997 17:38:50 +0200] rev 3838
tuned;
wenzelm [Fri, 10 Oct 1997 17:10:12 +0200] rev 3837
fixed dots;
wenzelm [Fri, 10 Oct 1997 16:29:41 +0200] rev 3836
fixed dots;
wenzelm [Fri, 10 Oct 1997 15:52:12 +0200] rev 3835
fixed dots;
wenzelm [Fri, 10 Oct 1997 15:51:38 +0200] rev 3834
BAD_space_explode;
wenzelm [Fri, 10 Oct 1997 15:51:14 +0200] rev 3833
tuned;
more accesses to long name;
wenzelm [Fri, 10 Oct 1997 15:50:46 +0200] rev 3832
fixed space_explode, old one retained as BAD_space_explode;
added split_lines;
wenzelm [Fri, 10 Oct 1997 15:48:43 +0200] rev 3831
scan_longid moved to Syntax/lexicon.ML;
wenzelm [Fri, 10 Oct 1997 15:48:10 +0200] rev 3830
constify: qualified is const;
wenzelm [Fri, 10 Oct 1997 15:47:41 +0200] rev 3829
added longid syntax;
wenzelm [Fri, 10 Oct 1997 15:46:50 +0200] rev 3828
added longid;
wenzelm [Fri, 10 Oct 1997 15:44:48 +0200] rev 3827
decode: qualified is always const;
wenzelm [Fri, 10 Oct 1997 14:51:58 +0200] rev 3826
tuned;
wenzelm [Thu, 09 Oct 1997 18:01:27 +0200] rev 3825
\n at end;
wenzelm [Thu, 09 Oct 1997 17:45:03 +0200] rev 3824
ensure that dots in formulas are followed by non-idents;
wenzelm [Thu, 09 Oct 1997 17:20:15 +0200] rev 3823
*** empty log message ***
wenzelm [Thu, 09 Oct 1997 15:06:49 +0200] rev 3822
no longer handles consts "" -- use syntax instead;
pretty printer: changed order of mixfix annotation preference (again!);
wenzelm [Thu, 09 Oct 1997 15:04:21 +0200] rev 3821
removed open;
wenzelm [Thu, 09 Oct 1997 15:03:06 +0200] rev 3820
fixed infix syntax;
wenzelm [Thu, 09 Oct 1997 15:01:11 +0200] rev 3819
added TLA stuff;
wenzelm [Thu, 09 Oct 1997 15:00:41 +0200] rev 3818
fixed oracle;
wenzelm [Thu, 09 Oct 1997 14:59:36 +0200] rev 3817
removed declIffOracle;
wenzelm [Thu, 09 Oct 1997 14:56:52 +0200] rev 3816
changed preference order of prtab entries;
wenzelm [Thu, 09 Oct 1997 14:55:24 +0200] rev 3815
fixed infix syntax;
wenzelm [Thu, 09 Oct 1997 14:55:05 +0200] rev 3814
improved oracles: named, many per theory;
name spaces: thmK, oracleK;
wenzelm [Thu, 09 Oct 1997 14:53:31 +0200] rev 3813
improved oracle: name;
optional begin after thy header, with warning;
wenzelm [Thu, 09 Oct 1997 14:52:36 +0200] rev 3812
fixed get_axiom, invoke_oracle;
improved Oracle deriv;
wenzelm [Thu, 09 Oct 1997 14:51:10 +0200] rev 3811
print_theory: added oracles;
wenzelm [Thu, 09 Oct 1997 14:50:39 +0200] rev 3810
tuned exports;
tuned add_space;
tuned print_sg;
fixed "op ==>" syntax;
wenzelm [Thu, 09 Oct 1997 14:39:44 +0200] rev 3809
fixed axiom names;
wenzelm [Wed, 08 Oct 1997 12:15:59 +0200] rev 3808
symbols syntax;
wenzelm [Wed, 08 Oct 1997 11:50:33 +0200] rev 3807
A formalization of TLA in HOL -- by Stephan Merz;
wenzelm [Tue, 07 Oct 1997 18:02:42 +0200] rev 3806
improved types of add_XXX funs (xtyp etc.);
wenzelm [Tue, 07 Oct 1997 18:02:02 +0200] rev 3805
improved types of add_XXX funs (xtyp etc.);
tuned comments;
tuned msgs;
improved merge: no longer raises ERROR, but TERM;
wenzelm [Tue, 07 Oct 1997 17:58:50 +0200] rev 3804
tuned decode;
wenzelm [Tue, 07 Oct 1997 17:58:01 +0200] rev 3803
tuned internal mapping table;
improved merge: 2nd overrides 1st;
wenzelm [Tue, 07 Oct 1997 17:08:48 +0200] rev 3802
tuned;
wenzelm [Tue, 07 Oct 1997 17:06:05 +0200] rev 3801
tuned warning msg;
wenzelm [Tue, 07 Oct 1997 12:37:53 +0200] rev 3800
tuned;
wenzelm [Tue, 07 Oct 1997 12:29:34 +0200] rev 3799
The Isabelle Logo;
wenzelm [Mon, 06 Oct 1997 20:00:31 +0200] rev 3798
fixed 'begin';
wenzelm [Mon, 06 Oct 1997 19:39:40 +0200] rev 3797
optional begin keyword;
wenzelm [Mon, 06 Oct 1997 19:16:57 +0200] rev 3796
"->" made syntax;
wenzelm [Mon, 06 Oct 1997 19:15:22 +0200] rev 3795
eliminated raise_term;
wenzelm [Mon, 06 Oct 1997 19:15:02 +0200] rev 3794
eliminated raise_term, raise_typ;
wenzelm [Mon, 06 Oct 1997 19:13:55 +0200] rev 3793
add_arities_i;
wenzelm [Mon, 06 Oct 1997 19:13:29 +0200] rev 3792
TODO: handle internal / external names;
wenzelm [Mon, 06 Oct 1997 19:11:56 +0200] rev 3791
now supports qualified names (intern vs. extern) !!!
added long_names: bool ref (initially false);
new internal forms: add_classes_i, add_classrel_i, add_defsort_i,
add_arities_i;
rep_sg: added path, spaces;
added pretty_sort (uses proper syntax);
improved print_sg;
eliminated raise_term, raise_typ;
wenzelm [Mon, 06 Oct 1997 19:07:14 +0200] rev 3790
eliminated raise_term, raise_typ;
tuned get_sort, decode_types, infer_types to accomodate qualified names;
wenzelm [Mon, 06 Oct 1997 18:59:49 +0200] rev 3789
tuned read_cterms;
wenzelm [Mon, 06 Oct 1997 18:57:17 +0200] rev 3788
eliminated raise_term, raise_typ;
new internal forms: add_inst_subclass_i, add_inst_arity_i;
wenzelm [Mon, 06 Oct 1997 18:43:32 +0200] rev 3787
new internal forms: add_classes_i, add_classrel_i, add_defsort_i, add_arities_i
added add_path, add_space;
eliminated raise_term;
wenzelm [Mon, 06 Oct 1997 18:41:39 +0200] rev 3786
tuned;
wenzelm [Mon, 06 Oct 1997 18:41:09 +0200] rev 3785
now uses new Sign.pretty_sort;
wenzelm [Mon, 06 Oct 1997 18:40:24 +0200] rev 3784
eliminated raise_term, raise_typ;
wenzelm [Mon, 06 Oct 1997 18:39:54 +0200] rev 3783
now uses Syntax.simple_str_of_sort;
wenzelm [Mon, 06 Oct 1997 18:39:25 +0200] rev 3782
added simple_str_of_sort;