Sat, 17 Sep 2005 01:50:01 +0200 huffman use interpretation command
Fri, 16 Sep 2005 23:55:23 +0200 huffman add HOLCF entries for pcpodef, cont_proc, fixrec;
Fri, 16 Sep 2005 23:01:29 +0200 wenzelm converted to Isar theory format;
Fri, 16 Sep 2005 21:02:15 +0200 obua fixed HOL-light/Isabelle syntax incompatability via more protect_xxx functions
Fri, 16 Sep 2005 20:30:44 +0200 huffman add header
Fri, 16 Sep 2005 16:07:22 +0200 ballarin tuned
Fri, 16 Sep 2005 14:46:31 +0200 ballarin interpretation uses primitive goal interface
Fri, 16 Sep 2005 14:44:52 +0200 ballarin tuned
Fri, 16 Sep 2005 11:39:09 +0200 paulson PARTIAL conversion to Vampire8
Fri, 16 Sep 2005 11:38:49 +0200 paulson catching exception Io
Fri, 16 Sep 2005 02:20:50 +0200 huffman rearranged
Fri, 16 Sep 2005 01:42:57 +0200 huffman use mem operator
Fri, 16 Sep 2005 01:34:53 +0200 huffman fix names in hypreal_arith.ML
Thu, 15 Sep 2005 23:53:33 +0200 huffman merge Hyperreal/Transfer.thy and Hyperreal/StarType.thy into Hyperreal/StarDef.thy
Thu, 15 Sep 2005 23:46:22 +0200 huffman merged Transfer.thy and StarType.thy into StarDef.thy; renamed Ifun2_of to starfun2; cleaned up
Thu, 15 Sep 2005 23:16:04 +0200 huffman add header
Thu, 15 Sep 2005 22:16:23 +0200 chaieb The SMLNJ Problem fixed...
Thu, 15 Sep 2005 20:38:47 +0200 chaieb getting it work for SMLNJ
Thu, 15 Sep 2005 20:27:48 +0200 wenzelm * Improved efficiency of the Simplifier etc.;
Thu, 15 Sep 2005 20:25:04 +0200 wenzelm incorporated into NEWS;
Thu, 15 Sep 2005 20:24:53 +0200 wenzelm incorporated HOL/Hyperreal/CHANGES;
Thu, 15 Sep 2005 17:46:00 +0200 paulson massive tidy-up and simplification
Thu, 15 Sep 2005 17:45:17 +0200 paulson moving Commutative_Ring to the correct theory
Thu, 15 Sep 2005 17:44:53 +0200 paulson comment
Thu, 15 Sep 2005 17:18:57 +0200 wenzelm poly -doDisplay;
Thu, 15 Sep 2005 17:17:06 +0200 wenzelm TableFun/Symtab: curried lookup and update;
Thu, 15 Sep 2005 17:17:05 +0200 wenzelm TableFun/Symtab: curried lookup and update;
Thu, 15 Sep 2005 17:17:04 +0200 wenzelm fixed type;
Thu, 15 Sep 2005 17:17:03 +0200 wenzelm fixed ML;
Thu, 15 Sep 2005 17:17:02 +0200 wenzelm The Hebrew Alef-Bet -- Unicode example;
Thu, 15 Sep 2005 17:17:01 +0200 wenzelm added Hebrew.thy;
Thu, 15 Sep 2005 17:16:56 +0200 wenzelm TableFun/Symtab: curried lookup and update;
Thu, 15 Sep 2005 17:16:55 +0200 wenzelm fixed document;
Thu, 15 Sep 2005 17:16:54 +0200 wenzelm added HOL/ex/Hebrew.thy;
Thu, 15 Sep 2005 17:16:53 +0200 wenzelm obsolete;
Thu, 15 Sep 2005 17:16:53 +0200 wenzelm command 'thms_containing' has been discontinued in favour of 'find_theorems';
Thu, 15 Sep 2005 16:15:22 +0200 aspinall Revert previous attribute name change, problem can be avoided in JAXB.
Thu, 15 Sep 2005 13:36:10 +0200 wenzelm forget_proof: Sign.local_path o Sign.restore_naming ProtoPure.thy -- workaround to omission in locale goals;
Thu, 15 Sep 2005 13:35:21 +0200 wenzelm extend: NameSpace.default_naming;
Thu, 15 Sep 2005 11:15:52 +0200 paulson the experimental tagging system, and the usual tidying
Thu, 15 Sep 2005 10:33:35 +0200 aspinall Change PGIP attribute name class->messageclass to avoid Java keyword clash.
Thu, 15 Sep 2005 10:00:01 +0200 haftmann AList, the_*
Thu, 15 Sep 2005 08:16:22 +0200 haftmann fixed type annotation
Thu, 15 Sep 2005 07:35:38 +0200 haftmann added gen_list to Pretty module
Wed, 14 Sep 2005 23:55:49 +0200 wenzelm @{term [source] ...} in subsections probably more robust;
Wed, 14 Sep 2005 23:31:09 +0200 wenzelm tuned;
Wed, 14 Sep 2005 23:15:00 +0200 wenzelm hide: added option '(open)';
Wed, 14 Sep 2005 23:14:59 +0200 wenzelm imports Commutative_Ring instead of Main, since the latter hides our names;
Wed, 14 Sep 2005 23:14:58 +0200 wenzelm hide the rather generic names used in theory Commutative_Ring;
Wed, 14 Sep 2005 23:14:57 +0200 wenzelm renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
Wed, 14 Sep 2005 23:06:02 +0200 schirmer ... prem19
Wed, 14 Sep 2005 23:04:59 +0200 schirmer added prem10 - prem19
Wed, 14 Sep 2005 23:03:52 +0200 schirmer removed syntax fun_map_comp;
Wed, 14 Sep 2005 23:00:03 +0200 chaieb Unfortunately patched to use IntInf.int instead of just int (SML compatibility)
Wed, 14 Sep 2005 22:18:55 +0200 wenzelm Method comm_ring for proving equalities in commutative rings.
Wed, 14 Sep 2005 22:08:08 +0200 wenzelm tuned headers etc.;
Wed, 14 Sep 2005 22:04:38 +0200 wenzelm fixed some ML names;
Wed, 14 Sep 2005 22:04:37 +0200 wenzelm imports Commutative_Ring;
Wed, 14 Sep 2005 22:04:36 +0200 wenzelm HOL: method comm_ring;
Wed, 14 Sep 2005 22:04:35 +0200 wenzelm tuned;
(0) -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip