huffman [Sat, 16 Apr 2005 00:16:44 +0200] rev 15741
New file for theorems used by the domain package
nipkow [Fri, 15 Apr 2005 18:43:35 +0200] rev 15740
rermoved pointless example
paulson [Fri, 15 Apr 2005 18:16:05 +0200] rev 15739
yet more tidying up: removal of some references to Main
nipkow [Fri, 15 Apr 2005 17:03:35 +0200] rev 15738
*** empty log message ***
nipkow [Fri, 15 Apr 2005 14:14:24 +0200] rev 15737
New
paulson [Fri, 15 Apr 2005 13:35:53 +0200] rev 15736
more tidying up of the SPASS interface
ballarin [Fri, 15 Apr 2005 12:00:00 +0200] rev 15735
Removed most of the atp interface from Pure.
aspinall [Thu, 14 Apr 2005 19:30:57 +0200] rev 15734
Include automatic determination of poly version.
aspinall [Thu, 14 Apr 2005 19:16:07 +0200] rev 15733
Add RDISTDIR option used by Isabelle RPM.
nipkow [Thu, 14 Apr 2005 17:57:23 +0200] rev 15732
Added thm names
nipkow [Thu, 14 Apr 2005 17:57:04 +0200] rev 15731
Removed dir Orderings in Library
kleing [Thu, 14 Apr 2005 09:19:55 +0200] rev 15730
fix: added path to garbage
kleing [Thu, 14 Apr 2005 08:56:08 +0200] rev 15729
added LaTeXsugar
kleing [Thu, 14 Apr 2005 08:52:46 +0200] rev 15728
added Makefile and generated files to make document available for makedist
wenzelm [Wed, 13 Apr 2005 20:20:14 +0200] rev 15727
Locales: proper static binding of attribute syntax;
Attributes 'induct' and 'cases': support local type or set names;
wenzelm [Wed, 13 Apr 2005 18:51:39 +0200] rev 15726
*** MESSAGE REFERS TO PREVIOUS VERSION ***
support embedded values and static binding -- via implicit assignment
to src tokens (cf. assignable/assign/closure);
renamed ident/string/keyword to mk_ident/mk_string/mk_keyword;
added mk_name, mk_typ, mk_term, mk_fact, mk_attribute;
added type value with map_values etc.;
removed name_dummy, added general 'maybe' combinator;
added global/local_tyname/const;
added pretty_src, pretty_attribs;
added thm_sel (from attrib.ML);
wenzelm [Wed, 13 Apr 2005 18:51:28 +0200] rev 15725
*** MESSAGE REFERS TO PREVIOUS VERSION ***
added read_tyname/const;
wenzelm [Wed, 13 Apr 2005 18:50:08 +0200] rev 15724
*** MESSAGE REFERS TO PREVIOUS VERSION ***
ISABELLE_DOC_FORMAT setting specifies preferred document format;
some cleanup;
wenzelm [Wed, 13 Apr 2005 18:49:42 +0200] rev 15723
*** MESSAGE REFERS TO PREVIOUS VERSION ***
added declared_tyname/const and read_tyname/const;
removed certify_tyname/const;
added prep_ext_merge, nontriv_merge kept internal;
efficient subsig test;
wenzelm [Wed, 13 Apr 2005 18:49:22 +0200] rev 15722
*** MESSAGE REFERS TO PREVIOUS VERSION ***
Attrib.src;
removed Locale.multi_attribute (pass Attrib.src instead);
removed interpret(_i) (use have_i instead);
goals: more uniform treatment of after_qed, removed separate thy_mod of global goals;
wenzelm [Wed, 13 Apr 2005 18:49:07 +0200] rev 15721
*** MESSAGE REFERS TO PREVIOUS VERSION ***
removed type multi_attribute (store Attrib.src instead);
datatype elem/element(_i): Attrib.src instead of 'att;
removed map_attrib_element etc.;
added intern_attrib_elem(_expr);
added map_elem, map_values to economize code;
static binding of values in Attrib.src (cf. Args.closure, Attrib.crude_closure);
prep_facts: transfer internal facts;
wenzelm [Wed, 13 Apr 2005 18:48:52 +0200] rev 15720
*** MESSAGE REFERS TO PREVIOUS VERSION ***
Attrib.src, Method.src;
Sign.declared_tyname/const;
no Attrib.multi_attribute, pass Attrib.src directly to locales;
register_locally: Proof.interpret_i replaced by Proof.have_i;
wenzelm [Wed, 13 Apr 2005 18:48:39 +0200] rev 15719
*** MESSAGE REFERS TO PREVIOUS VERSION ***
type src = Args.src;
renamed local_attribute' to context_attribute;
added _i versions of global/local/context_attribute and separate intern/intern_src;
added crude_closure to produce argument closure without knowing facts in advance;
added 'attribute' to embed internal attributes into src;
removed multi_attribute etc.;
moved thm_sel to args.ML;
Scan.peek;
read_instantiate/'where'/'of': support arbitrary mix of external /
internal typ / term args, with proper treatment of static binding;
wenzelm [Wed, 13 Apr 2005 18:48:19 +0200] rev 15718
*** MESSAGE REFERS TO PREVIOUS VERSION ***
ISABELLE_DOC_FORMAT;
tuned;
wenzelm [Wed, 13 Apr 2005 18:48:05 +0200] rev 15717
*** MESSAGE REFERS TO PREVIOUS VERSION ***
ISABELLE_DOC_FORMAT;
wenzelm [Wed, 13 Apr 2005 18:47:53 +0200] rev 15716
*** MESSAGE REFERS TO PREVIOUS VERSION ***
Sign.prep_ext_merge;
wenzelm [Wed, 13 Apr 2005 18:47:43 +0200] rev 15715
*** MESSAGE REFERS TO PREVIOUS VERSION ***
added datatype interval, improved thm selections;
wenzelm [Wed, 13 Apr 2005 18:47:01 +0200] rev 15714
*** MESSAGE REFERS TO PREVIOUS VERSION ***
removed uterm, added 'maybe';
Attrib.src;
improved thm_sel;
wenzelm [Wed, 13 Apr 2005 18:46:52 +0200] rev 15713
*** MESSAGE REFERS TO PREVIOUS VERSION ***
type src = Args.src;
Drule.add_used;
wenzelm [Wed, 13 Apr 2005 18:46:39 +0200] rev 15712
*** MESSAGE REFERS TO PREVIOUS VERSION ***
removed uterm;
tuned;
wenzelm [Wed, 13 Apr 2005 18:46:30 +0200] rev 15711
*** MESSAGE REFERS TO PREVIOUS VERSION ***
Attrib.src;
ISABELLE_DOC_FORMAT;
wenzelm [Wed, 13 Apr 2005 18:46:22 +0200] rev 15710
*** MESSAGE REFERS TO PREVIOUS VERSION ***
Scan.peek;
Args.global/local_const/tyname (static binding!);
wenzelm [Wed, 13 Apr 2005 18:46:12 +0200] rev 15709
*** MESSAGE REFERS TO PREVIOUS VERSION ***
use args.ML, attrib.ML earlier;
wenzelm [Wed, 13 Apr 2005 18:46:04 +0200] rev 15708
*** MESSAGE REFERS TO PREVIOUS VERSION ***
Scan.peek;
Args.local_tyname, Args.local_const;
wenzelm [Wed, 13 Apr 2005 18:45:52 +0200] rev 15707
*** MESSAGE REFERS TO PREVIOUS VERSION ***
Method.src;
wenzelm [Wed, 13 Apr 2005 18:45:38 +0200] rev 15706
*** MESSAGE REFERS TO PREVIOUS VERSION ***
Args.global_const (static binding!);
wenzelm [Wed, 13 Apr 2005 18:45:25 +0200] rev 15705
*** MESSAGE REFERS TO PREVIOUS VERSION ***
Attrib.src;
wenzelm [Wed, 13 Apr 2005 18:45:09 +0200] rev 15704
*** MESSAGE REFERS TO PREVIOUS VERSION ***
Attrib.src;
Args.maybe;
wenzelm [Wed, 13 Apr 2005 18:34:22 +0200] rev 15703
*** empty log message ***
paulson [Wed, 13 Apr 2005 09:48:41 +0200] rev 15702
new signalling primmitives for sml/nj compatibility
nipkow [Tue, 12 Apr 2005 13:38:08 +0200] rev 15701
*** empty log message ***
paulson [Tue, 12 Apr 2005 11:08:25 +0200] rev 15700
tweaks mainly to achieve sml/nj compatibility
paulson [Tue, 12 Apr 2005 11:07:42 +0200] rev 15699
fixing an incompatibility with Posix.IO.mkTextReader
paulson [Mon, 11 Apr 2005 16:25:53 +0200] rev 15698
auto update
paulson [Mon, 11 Apr 2005 16:25:31 +0200] rev 15697
removal of Main and other tidying up
ballarin [Mon, 11 Apr 2005 12:34:34 +0200] rev 15696
First release of interpretation commands.
nipkow [Mon, 11 Apr 2005 12:18:27 +0200] rev 15695
tuned
nipkow [Mon, 11 Apr 2005 12:14:48 +0200] rev 15694
added \restriction
nipkow [Mon, 11 Apr 2005 12:14:23 +0200] rev 15693
tuned Map, renamed lex stuff in List.
nipkow [Sun, 10 Apr 2005 17:20:03 +0200] rev 15692
Added lots of AMS harpoons
nipkow [Sun, 10 Apr 2005 17:19:03 +0200] rev 15691
_(_|_) is now override_on
nipkow [Sun, 10 Apr 2005 11:42:07 +0200] rev 15690
tuned
nipkow [Sun, 10 Apr 2005 11:41:29 +0200] rev 15689
section on qmark
paulson [Sat, 09 Apr 2005 16:27:11 +0200] rev 15688
fixed the syntax of infix declarations
wenzelm [Sat, 09 Apr 2005 15:36:02 +0200] rev 15687
thmref: selection syntax;
wenzelm [Sat, 09 Apr 2005 15:35:37 +0200] rev 15686
update syntax of 'where' and 'of';
wenzelm [Sat, 09 Apr 2005 15:34:38 +0200] rev 15685
added PDF_VIEWER, ISABELLE_DOC_FORMAT;
paulson [Fri, 08 Apr 2005 18:43:39 +0200] rev 15684
Reconstruction code, now packaged to avoid name clashes
paulson [Fri, 08 Apr 2005 10:50:02 +0200] rev 15683
temporarily removed ATP code
paulson [Thu, 07 Apr 2005 18:44:45 +0200] rev 15682
removed bad code
quigley [Thu, 07 Apr 2005 18:35:21 +0200] rev 15681
Changed prob1.dfg to prob_1.dfg
quigley [Thu, 07 Apr 2005 18:33:56 +0200] rev 15680
Got rid of Main.thy reference
quigley [Thu, 07 Apr 2005 18:20:04 +0200] rev 15679
Integrating the reconstruction files into the building of HOL
quigley [Thu, 07 Apr 2005 17:45:51 +0200] rev 15678
Reconstruction.thy and IsaMakefile updated
nipkow [Thu, 07 Apr 2005 14:07:40 +0200] rev 15677
*** empty log message ***
paulson [Thu, 07 Apr 2005 13:29:41 +0200] rev 15676
new meta-level rules
nipkow [Thu, 07 Apr 2005 10:22:55 +0200] rev 15675
*** empty log message ***
wenzelm [Thu, 07 Apr 2005 09:51:17 +0200] rev 15674
reverted renaming of Some/None in comments and strings;
wenzelm [Thu, 07 Apr 2005 09:28:16 +0200] rev 15673
added term_8;
wenzelm [Thu, 07 Apr 2005 09:28:03 +0200] rev 15672
added get_axiom_i, invoke_oracle_i;
wenzelm [Thu, 07 Apr 2005 09:27:50 +0200] rev 15671
Drule.add_used;
wenzelm [Thu, 07 Apr 2005 09:27:33 +0200] rev 15670
invalidated former constructors None/OPTION to prevent accidental use as match-all patterns!
wenzelm [Thu, 07 Apr 2005 09:27:20 +0200] rev 15669
added add_used; include tpairs;
wenzelm [Thu, 07 Apr 2005 09:27:09 +0200] rev 15668
improved exn_message;
wenzelm [Thu, 07 Apr 2005 09:26:55 +0200] rev 15667
Thm.invoke_oracle_i;
wenzelm [Thu, 07 Apr 2005 09:26:48 +0200] rev 15666
Scan.peek;
wenzelm [Thu, 07 Apr 2005 09:26:40 +0200] rev 15665
tuned updates, added map_entry;
wenzelm [Thu, 07 Apr 2005 09:26:29 +0200] rev 15664
added some, peek, trace'; tuned;
wenzelm [Thu, 07 Apr 2005 09:26:18 +0200] rev 15663
added header;
wenzelm [Thu, 07 Apr 2005 09:26:10 +0200] rev 15662
improved comments;
wenzelm [Thu, 07 Apr 2005 09:25:33 +0200] rev 15661
reverted renaming of Some/None in comments and strings;
wenzelm [Thu, 07 Apr 2005 09:24:35 +0200] rev 15660
handle Option instead of OPTION;
nipkow [Wed, 06 Apr 2005 18:13:30 +0200] rev 15659
updated it
quigley [Wed, 06 Apr 2005 12:01:37 +0200] rev 15658
watcher.ML and watcher.sig changed. Debug files now write to tmp.
quigley [Tue, 05 Apr 2005 16:32:47 +0200] rev 15657
Current version of res_atp.ML - causes an error when I run it. C.Q.
paulson [Tue, 05 Apr 2005 13:05:38 +0200] rev 15656
lexicographic order by Norbert Voelker
paulson [Tue, 05 Apr 2005 13:05:20 +0200] rev 15655
arg_cong2 by Norbert Voelker
nipkow [Tue, 05 Apr 2005 08:03:52 +0200] rev 15654
*** empty log message ***
quigley [Mon, 04 Apr 2005 18:43:18 +0200] rev 15653
Updated to add watcher code.
quigley [Mon, 04 Apr 2005 18:39:45 +0200] rev 15652
CVSfj
-------------------------------------------------------------------
---------------------------------------------------------------
Temporarily added until res_axioms.ML is altered.
huffman [Sat, 02 Apr 2005 00:33:51 +0200] rev 15651
Replaced continuity solver with new continuity simproc. Also removed cont lemmas from simp set, so that the simproc actually gets used.
huffman [Sat, 02 Apr 2005 00:12:38 +0200] rev 15650
converted to new-style theory
huffman [Fri, 01 Apr 2005 23:44:41 +0200] rev 15649
convert to new-style theory
paulson [Fri, 01 Apr 2005 21:04:00 +0200] rev 15648
x-symbols and other tidying
skalberg [Fri, 01 Apr 2005 18:59:17 +0200] rev 15647
Updated import configuration.
gagern [Fri, 01 Apr 2005 18:40:14 +0200] rev 15646
bring make to delete files on error
paulson [Fri, 01 Apr 2005 11:12:39 +0200] rev 15645
patch to get it working again
quigley [Thu, 31 Mar 2005 20:12:54 +0200] rev 15644
*** empty log message ***
quigley [Thu, 31 Mar 2005 19:47:30 +0200] rev 15643
*** empty log message ***
quigley [Thu, 31 Mar 2005 19:29:26 +0200] rev 15642
*** empty log message ***
huffman [Thu, 31 Mar 2005 03:03:22 +0200] rev 15641
added theorems eta_cfun and cont2cont_eta
huffman [Thu, 31 Mar 2005 03:01:21 +0200] rev 15640
chfin now a subclass of po, proved instance chfin < cpo
huffman [Thu, 31 Mar 2005 02:52:49 +0200] rev 15639
cleaned up some proofs
huffman [Thu, 31 Mar 2005 02:44:46 +0200] rev 15638
fixed bug in prj' function
huffman [Thu, 31 Mar 2005 00:10:35 +0200] rev 15637
changed comments to text blocks, cleaned up a few proofs
paulson [Wed, 30 Mar 2005 08:33:41 +0200] rev 15636
converted from DOS to UNIX format
paulson [Tue, 29 Mar 2005 12:30:48 +0200] rev 15635
converted HOL-Subst to tactic scripts
paulson [Mon, 28 Mar 2005 16:19:56 +0200] rev 15634
conversion of UNITY to Isar scripts
paulson [Sat, 26 Mar 2005 18:20:29 +0100] rev 15633
new display of theory stamps
gagern [Sat, 26 Mar 2005 16:14:17 +0100] rev 15632
op vor infix-Konstruktoren im datatype binding zum besseren Parsen
kleing [Sat, 26 Mar 2005 00:01:56 +0100] rev 15631
use Library/Multiset instead of own definition
kleing [Sat, 26 Mar 2005 00:00:56 +0100] rev 15630
fixed typo (multiset_append)
moved multiset_of_complement_union from ex/Sorting
aspinall [Fri, 25 Mar 2005 17:47:11 +0100] rev 15629
Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
paulson [Fri, 25 Mar 2005 16:20:57 +0100] rev 15628
tidied up
aspinall [Fri, 25 Mar 2005 14:14:01 +0100] rev 15627
Revert previous change (but leave comments).
aspinall [Fri, 25 Mar 2005 14:04:42 +0100] rev 15626
Support new PGIP commands redostep, redoitem
aspinall [Fri, 25 Mar 2005 13:03:47 +0100] rev 15625
Support non-standard file: URL syntax, temporarily.
ballarin [Thu, 24 Mar 2005 17:03:37 +0100] rev 15624
Further work on interpretation commands. New command `interpret' for
interpretation in proof contexts.
ballarin [Thu, 24 Mar 2005 16:36:40 +0100] rev 15623
*** empty log message ***
ballarin [Thu, 24 Mar 2005 16:34:15 +0100] rev 15622
Transitivity reasoner ignores types amenable to linear arithmetic.
These are currently nat, int, real.
Fixed IsaMakefile.
paulson [Thu, 24 Mar 2005 10:59:21 +0100] rev 15621
COMMENT IN WRONG PLACE
paulson [Wed, 23 Mar 2005 12:09:18 +0100] rev 15620
replaced bool by a new datatype "bit" for binary numerals
paulson [Wed, 23 Mar 2005 12:08:52 +0100] rev 15619
temporary removal of Import
paulson [Wed, 23 Mar 2005 12:08:27 +0100] rev 15618
tidied
paulson [Tue, 22 Mar 2005 16:32:25 +0100] rev 15617
auto update
paulson [Tue, 22 Mar 2005 16:31:51 +0100] rev 15616
deleted a pointless comment
paulson [Tue, 22 Mar 2005 16:30:43 +0100] rev 15615
ensuring that "equal" is not a function
paulson [Fri, 18 Mar 2005 14:31:50 +0100] rev 15614
auto update
paulson [Thu, 17 Mar 2005 15:12:03 +0100] rev 15613
meson now checks that problems are first-order
nipkow [Thu, 17 Mar 2005 12:19:50 +0100] rev 15612
added string_of_term
webertj [Thu, 17 Mar 2005 01:40:18 +0100] rev 15611
Bugfix related to the interpretation of IDT constructors
paulson [Tue, 15 Mar 2005 17:07:41 +0100] rev 15610
more concise ASCII escaping
huffman [Mon, 14 Mar 2005 20:30:43 +0100] rev 15609
fixed syntax for Let <x,y> = a in e
paulson [Mon, 14 Mar 2005 17:04:10 +0100] rev 15608
bug fixes involving typechecking clauses
huffman [Sat, 12 Mar 2005 00:07:05 +0100] rev 15607
removed theorems about Sinl_Rep and Sinr_Rep
huffman [Fri, 11 Mar 2005 23:58:31 +0100] rev 15606
simplified some definitions, many proofs are much shorter
webertj [Fri, 11 Mar 2005 16:56:48 +0100] rev 15605
minor Library.option related modifications
webertj [Fri, 11 Mar 2005 16:35:06 +0100] rev 15604
code reformatted
webertj [Fri, 11 Mar 2005 16:08:21 +0100] rev 15603
code reformatted
huffman [Fri, 11 Mar 2005 00:45:07 +0100] rev 15602
fixed bug: domain package can now define three or more mutually recursive types simultaneously
huffman [Fri, 11 Mar 2005 00:43:52 +0100] rev 15601
domain package now permits indirect recursion with these type constructors: *, ->, ++, **, u
huffman [Thu, 10 Mar 2005 20:22:45 +0100] rev 15600
fixed filename in header
huffman [Thu, 10 Mar 2005 20:19:55 +0100] rev 15599
instance u :: (cpo) pcpo -- argument type no longer needs to be pointed
ballarin [Thu, 10 Mar 2005 17:48:36 +0100] rev 15598
Registrations of global locale interpretations: improved, better naming.
ballarin [Thu, 10 Mar 2005 09:11:57 +0100] rev 15597
Debugging code (error_depth) removed.
ballarin [Wed, 09 Mar 2005 18:44:52 +0100] rev 15596
First version of global registration command.
obua [Tue, 08 Mar 2005 16:02:52 +0100] rev 15595
fix integer overflow in numeral syntax for SML NJ.
huffman [Tue, 08 Mar 2005 00:45:58 +0100] rev 15594
fixed variable name
huffman [Tue, 08 Mar 2005 00:32:10 +0100] rev 15593
reordered and arranged for document generation, cleaned up some proofs
huffman [Tue, 08 Mar 2005 00:28:46 +0100] rev 15592
removed Cprod3_lemma1 and Cprod3_lemma2
huffman [Tue, 08 Mar 2005 00:18:22 +0100] rev 15591
reordered and arranged for document generation, cleaned up some proofs
huffman [Tue, 08 Mar 2005 00:15:01 +0100] rev 15590
added subsection headings, cleaned up some proofs
huffman [Tue, 08 Mar 2005 00:11:49 +0100] rev 15589
reordered and arranged for document generation, cleaned up some proofs
huffman [Tue, 08 Mar 2005 00:00:49 +0100] rev 15588
arranged for document generation, cleaned up some proofs
huffman [Mon, 07 Mar 2005 23:54:01 +0100] rev 15587
added subsections and text for document generation
huffman [Mon, 07 Mar 2005 23:30:06 +0100] rev 15586
Added dependency document/root.tex, and -g true option to isatool; document generation should work now.
webertj [Mon, 07 Mar 2005 19:41:04 +0100] rev 15585
HTML 4.01 Transitional conformity
webertj [Mon, 07 Mar 2005 19:30:53 +0100] rev 15584
refute_params: default value itself=1 added (for type classes)
webertj [Mon, 07 Mar 2005 19:25:13 +0100] rev 15583
HTML 4.01 Transitional conformity
webertj [Mon, 07 Mar 2005 19:17:07 +0100] rev 15582
HTML 4.01 Transitional conformity
paulson [Mon, 07 Mar 2005 18:40:36 +0100] rev 15581
now checks for higher-order vars
obua [Mon, 07 Mar 2005 18:19:55 +0100] rev 15580
Cleaning up HOL/Matrix
paulson [Mon, 07 Mar 2005 16:55:36 +0100] rev 15579
Tools/meson.ML: signature, structure and "open" rather than "local"
huffman [Fri, 04 Mar 2005 23:25:06 +0100] rev 15578
add header
huffman [Fri, 04 Mar 2005 23:23:47 +0100] rev 15577
fix headers
huffman [Fri, 04 Mar 2005 23:12:36 +0100] rev 15576
converted to new-style theories, and combined numbered files
huffman [Fri, 04 Mar 2005 18:53:46 +0100] rev 15575
document generation for HOLCF
skalberg [Fri, 04 Mar 2005 15:07:34 +0100] rev 15574
Removed practically all references to Library.foldr.
paulson [Fri, 04 Mar 2005 11:44:26 +0100] rev 15573
new first_order test
paulson [Fri, 04 Mar 2005 10:58:04 +0100] rev 15572
removed dead code
webertj [Thu, 03 Mar 2005 17:22:46 +0100] rev 15571
interpreter for Finite_Set.Finites added
skalberg [Thu, 03 Mar 2005 12:43:01 +0100] rev 15570
Move towards standard functions.
nipkow [Thu, 03 Mar 2005 09:22:35 +0100] rev 15569
fixed proof
huffman [Thu, 03 Mar 2005 01:37:32 +0100] rev 15568
converted to new-style theory
huffman [Thu, 03 Mar 2005 00:42:04 +0100] rev 15567
converted to new-style theory
huffman [Wed, 02 Mar 2005 23:58:02 +0100] rev 15566
converted to new-style theory
huffman [Wed, 02 Mar 2005 23:28:17 +0100] rev 15565
converted to new-style theory
huffman [Wed, 02 Mar 2005 23:15:16 +0100] rev 15564
converted to new-style theory
huffman [Wed, 02 Mar 2005 22:57:08 +0100] rev 15563
converted to new-style theory
huffman [Wed, 02 Mar 2005 22:30:00 +0100] rev 15562
converted to new-style theory
nipkow [Wed, 02 Mar 2005 12:06:15 +0100] rev 15561
another reorganization of setsums and intervals
dixon [Wed, 02 Mar 2005 10:33:10 +0100] rev 15560
lucas - fixed bug with name capture variables bound outside redex could (previously)conflict with scheme variables that occur in the conditions of an equation, and which were renamed to avoid conflict with another instantiation. This has now been fixed.
paulson [Wed, 02 Mar 2005 10:21:17 +0100] rev 15559
obscured the e-mail address lcp@cl
paulson [Wed, 02 Mar 2005 10:02:21 +0100] rev 15558
new lemmas int_diff_cases
huffman [Wed, 02 Mar 2005 00:56:41 +0100] rev 15557
eliminated deps for removed files
huffman [Wed, 02 Mar 2005 00:55:12 +0100] rev 15556
merged into Discrete.thy
huffman [Wed, 02 Mar 2005 00:54:06 +0100] rev 15555
converted to new-style theory
nipkow [Tue, 01 Mar 2005 18:48:52 +0100] rev 15554
integrated Jeremy's FiniteLib
kleing [Tue, 01 Mar 2005 05:44:13 +0100] rev 15553
spider dogding
obua [Mon, 28 Feb 2005 18:29:55 +0100] rev 15552
added setsum_diff1' which holds in more general cases than setsum_diff1
paulson [Mon, 28 Feb 2005 13:10:36 +0100] rev 15551
unfold theorems for trancl and rtrancl
dixon [Sun, 27 Feb 2005 00:00:40 +0100] rev 15550
lucas - added more comments and an extra type to clarify the code.
berghofe [Wed, 23 Feb 2005 15:19:00 +0100] rev 15549
Modified node_trans to avoid duplication of signature stamps
when undoing.
webertj [Wed, 23 Feb 2005 15:00:03 +0100] rev 15548
exception SAME removed
webertj [Wed, 23 Feb 2005 14:04:53 +0100] rev 15547
major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
nipkow [Wed, 23 Feb 2005 10:23:22 +0100] rev 15546
suminf -> \<Sum>
dixon [Tue, 22 Feb 2005 18:42:22 +0100] rev 15545
Lucas - fixed bug in zero_var_indexes: it was ignoring vars in the flex-flex pairs. These are now taken into account.
paulson [Tue, 22 Feb 2005 13:05:47 +0100] rev 15544
removed redundant lemmas and simprules
nipkow [Tue, 22 Feb 2005 10:54:30 +0100] rev 15543
more setsum tuning
nipkow [Mon, 21 Feb 2005 19:23:46 +0100] rev 15542
more fine tuniung
nipkow [Mon, 21 Feb 2005 18:04:28 +0100] rev 15541
fixed proof
nipkow [Mon, 21 Feb 2005 15:57:45 +0100] rev 15540
removed superfluous setsum_constant
nipkow [Mon, 21 Feb 2005 15:04:10 +0100] rev 15539
comprehensive cleanup, replacing sumr by setsum
dixon [Sat, 19 Feb 2005 18:44:34 +0100] rev 15538
lucas - re-arranged code and added comments. Also added check to make sure the subgoal that we are being applied to exists. If it does not, empty seq is returned.
nipkow [Fri, 18 Feb 2005 15:20:27 +0100] rev 15537
continued eliminating sumr
nipkow [Fri, 18 Feb 2005 11:48:53 +0100] rev 15536
starting to get rid of sumr
nipkow [Fri, 18 Feb 2005 11:48:42 +0100] rev 15535
tuning
nipkow [Wed, 16 Feb 2005 19:00:49 +0100] rev 15534
*** empty log message ***
berghofe [Tue, 15 Feb 2005 16:56:15 +0100] rev 15533
refine now provides specific cases "goal1" ... "goaln" for addressing
subgoals of a proof state.
paulson [Mon, 14 Feb 2005 10:24:58 +0100] rev 15532
simplified a proof
skalberg [Sun, 13 Feb 2005 17:15:14 +0100] rev 15531
Deleted Library.option type.
berghofe [Fri, 11 Feb 2005 18:51:00 +0100] rev 15530
Fully qualified refl and trans to avoid confusion with theorems
in Lattice_Locales.partial_order.
berghofe [Fri, 11 Feb 2005 17:11:24 +0100] rev 15529
Optimized present_tokens to produce fewer newlines when hiding proofs.
ballarin [Fri, 11 Feb 2005 10:03:41 +0100] rev 15528
New reference Toplevel.debug for verbose printing of exns.
kleing [Fri, 11 Feb 2005 04:36:22 +0100] rev 15527
update from Larry
nipkow [Thu, 10 Feb 2005 19:14:35 +0100] rev 15526
some stuff is now redundant.
nipkow [Thu, 10 Feb 2005 18:51:54 +0100] rev 15525
HOL.order -> Orderings.order due to restructering
nipkow [Thu, 10 Feb 2005 18:51:12 +0100] rev 15524
Moved oderings from HOL into the new Orderings.thy
berghofe [Thu, 10 Feb 2005 17:09:15 +0100] rev 15523
Added paper by M. Takahashi.
berghofe [Thu, 10 Feb 2005 17:08:45 +0100] rev 15522
Added proof of eta-postponement theorem (using parallel eta-reduction).
paulson [Thu, 10 Feb 2005 16:03:18 +0100] rev 15521
non-inductive fold1Set proofs
paulson [Thu, 10 Feb 2005 13:01:46 +0100] rev 15520
simplified a key lemma for foldSet
ballarin [Thu, 10 Feb 2005 12:06:40 +0100] rev 15519
Toplevel.debug for debugging in Isar.
berghofe [Thu, 10 Feb 2005 11:19:03 +0100] rev 15518
Fixed bug in select_thm.
berghofe [Thu, 10 Feb 2005 10:43:57 +0100] rev 15517
Subscripts for theorem lists now start at 1.
kleing [Thu, 10 Feb 2005 08:25:22 +0100] rev 15516
mention authors are acknowledged for isabelle-lemmas
kleing [Thu, 10 Feb 2005 08:21:40 +0100] rev 15515
more preview
kleing [Thu, 10 Feb 2005 07:47:06 +0100] rev 15514
pointer to isabelle-lemmas submission list
nipkow [Wed, 09 Feb 2005 18:51:02 +0100] rev 15513
added lattice_locales
nipkow [Wed, 09 Feb 2005 18:50:09 +0100] rev 15512
Extracted generic lattice stuff to new Lattice_Locales.thy
nipkow [Wed, 09 Feb 2005 18:49:29 +0100] rev 15511
New
paulson [Wed, 09 Feb 2005 18:32:28 +0100] rev 15510
new foldSet proofs
paulson [Wed, 09 Feb 2005 12:08:46 +0100] rev 15509
revised fold1 proofs
paulson [Wed, 09 Feb 2005 10:17:09 +0100] rev 15508
revised fold1 proofs
nipkow [Tue, 08 Feb 2005 18:32:34 +0100] rev 15507
cvs merge problem fixed
paulson [Tue, 08 Feb 2005 15:11:30 +0100] rev 15506
new treatment of fold1
nipkow [Tue, 08 Feb 2005 09:46:00 +0100] rev 15505
Fixed lattice defns
nipkow [Mon, 07 Feb 2005 18:20:46 +0100] rev 15504
*** empty log message ***
nipkow [Mon, 07 Feb 2005 08:02:49 +0100] rev 15503
fixed latex problems by including bigsqcap
nipkow [Mon, 07 Feb 2005 08:02:14 +0100] rev 15502
fixed latex problems