Mon, 11 May 2009 08:24:35 -0700 huffman removed redundant instance declarations inat :: linorder
Mon, 11 May 2009 17:08:31 +0200 haftmann merged
Mon, 11 May 2009 11:53:21 +0200 haftmann proper error handling for malformed code equations
Mon, 11 May 2009 11:53:21 +0200 haftmann corrected deletetion of code equations for constructors
Mon, 11 May 2009 10:53:19 +0200 haftmann clarified matter of "proper" flag in code equations
Mon, 11 May 2009 09:40:39 +0200 haftmann tuned interface of module Code_Unit
Mon, 11 May 2009 09:40:38 +0200 haftmann clarified terminilogy concerning nbe equations
Mon, 11 May 2009 09:40:38 +0200 haftmann simplified unoverload/overload policy in code generator preprocessor
Mon, 11 May 2009 15:05:17 +0100 paulson Change to lowercase path names as directed by local pagemasters
Sun, 10 May 2009 14:22:04 +0200 nipkow merged
Sun, 10 May 2009 14:21:41 +0200 nipkow fixed HOLCF proofs
Sat, 09 May 2009 09:17:45 +0200 haftmann merged
Sat, 09 May 2009 09:17:29 +0200 haftmann interface changes in linarith.ML
Sat, 09 May 2009 07:25:45 +0200 nipkow merged
Sat, 09 May 2009 07:25:22 +0200 nipkow lemmas by Andreas Lochbihler
Fri, 08 May 2009 19:20:00 +0200 nipkow merged
Fri, 08 May 2009 08:07:05 +0200 nipkow merged
Fri, 08 May 2009 08:06:43 +0200 nipkow more lemmas
Fri, 08 May 2009 16:19:51 -0700 huffman rename constant sq_le to below; rename class sq_ord to below; less->below in many lemma names
Fri, 08 May 2009 19:28:11 +0100 chaieb fixed theorem statement
Fri, 08 May 2009 14:03:24 +0100 chaieb merged
Fri, 08 May 2009 14:02:33 +0100 chaieb Generalized distributivity theorems of radicals over multiplication, division and inverses
Fri, 08 May 2009 13:38:21 +0200 haftmann proper structure name
Fri, 08 May 2009 13:34:27 +0200 haftmann localized (complete) partial order classes
Fri, 08 May 2009 10:59:11 +0200 haftmann dropped legacy ml theorem binding
Fri, 08 May 2009 09:48:54 +0200 haftmann modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
Fri, 08 May 2009 09:48:07 +0200 haftmann modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
Fri, 08 May 2009 08:01:09 +0200 haftmann generalized simproc for mod
Fri, 08 May 2009 08:00:13 +0200 haftmann explicit method linarith
Fri, 08 May 2009 08:00:11 +0200 haftmann moved int_factor_simprocs.ML to theory Int
Thu, 07 May 2009 16:22:35 +0200 haftmann treat frees driectly by the LCF kernel
Thu, 07 May 2009 16:22:35 +0200 haftmann dropped explicit suppport for frees in evaluation conversion stack
Thu, 07 May 2009 16:22:34 +0200 haftmann no need for explicit delete declaration
Thu, 07 May 2009 16:22:34 +0200 haftmann better to have distinguished class for preorders
Thu, 07 May 2009 12:17:17 +0200 haftmann added theory for explicit equivalence relation in preorders
Thu, 07 May 2009 12:02:16 +0200 haftmann explicit type_name antiquotations
Thu, 07 May 2009 12:02:15 +0200 haftmann explicit type arguments in constants
Wed, 06 May 2009 19:42:27 +0200 haftmann merged
Wed, 06 May 2009 19:09:31 +0200 haftmann robustifed infrastructure for complex term syntax during code generation
Wed, 06 May 2009 19:09:31 +0200 haftmann proper structures for list and string code generation stuff
Wed, 06 May 2009 19:09:14 +0200 haftmann explicit type arguments in constants
Wed, 06 May 2009 19:09:14 +0200 haftmann confine term setup to Eval serialiser
Wed, 06 May 2009 16:10:12 +0200 haftmann adaptation replaces adaption
Wed, 06 May 2009 16:01:23 +0200 haftmann refined HOL string theories and corresponding ML fragments
Wed, 06 May 2009 16:01:07 +0200 haftmann adaptation replaces adaption
Wed, 06 May 2009 16:01:06 +0200 haftmann explicit type arguments in constants
Wed, 06 May 2009 16:01:06 +0200 haftmann refined HOL string theories and corresponding ML fragments
Wed, 06 May 2009 16:01:05 +0200 haftmann tuned description of overloading
Wed, 06 May 2009 16:01:05 +0200 haftmann confine term setup to Eval serialiser
Wed, 06 May 2009 16:01:05 +0200 haftmann updated generated file
Wed, 06 May 2009 19:15:40 +0200 nipkow new lemmas
Wed, 06 May 2009 09:58:24 +0200 nipkow merged
Wed, 06 May 2009 10:55:47 +1000 Timothy Bourke Prototype introiff option for find_theorems.
Wed, 06 May 2009 00:57:29 -0700 huffman replace cont2cont_apply with cont_apply; add new cont2cont lemmas
Wed, 06 May 2009 09:08:47 +0200 haftmann compatible with preorder; bot and top instances
Mon, 04 May 2009 23:45:58 +0200 immler updated generated files etc/isar-keywords.el and lib/jedit/isabelle.xml
Mon, 04 May 2009 23:44:11 +0200 immler tuned
Mon, 04 May 2009 23:37:39 +0200 immler added Philipp Meyer's implementation of AtpMinimal
Mon, 04 May 2009 14:49:51 +0200 haftmann removed code_name module
Mon, 04 May 2009 14:49:50 +0200 haftmann desymbolization with case selection
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip