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