Mon, 25 Mar 1996 11:13:59 +0100 nipkow added converse_converse
Mon, 25 Mar 1996 08:46:02 +0100 nipkow replaced "rules" by "primrec"
Sun, 24 Mar 1996 18:36:28 +0100 clasohm moved init_data to new public function set_current_thy
Fri, 22 Mar 1996 12:06:08 +0100 clasohm fixed incompatibility of add_to_parents with SML109's new Io exceptions
Thu, 21 Mar 1996 13:02:26 +0100 paulson Changes required by removal of the theory argument of Theorem
Thu, 21 Mar 1996 11:13:05 +0100 paulson Examples call gocls to make goal clauses
Thu, 21 Mar 1996 11:11:47 +0100 paulson Now labels the Horn and goal clauses to make the proof
Thu, 21 Mar 1996 11:09:47 +0100 paulson For the new version of name_thm. Now the same theorem
Thu, 21 Mar 1996 11:06:59 +0100 paulson name_thm no longer takes a theory argument, as the
Thu, 21 Mar 1996 11:05:34 +0100 paulson Printing & string functions moved to display.ML
Thu, 21 Mar 1996 11:04:36 +0100 paulson Now loads deriv.ML
Wed, 20 Mar 1996 18:43:08 +0100 paulson Includes deriv.ML and display.ML as dependencies
Wed, 20 Mar 1996 18:42:31 +0100 paulson New module for proof objects (deriviations)
Wed, 20 Mar 1996 18:40:57 +0100 paulson maketest now closes the output file
Wed, 20 Mar 1996 18:39:59 +0100 paulson New module for display/printing operations, taken from drule.ML
Wed, 20 Mar 1996 18:36:59 +0100 paulson Describes proof objects and Deriv module
Wed, 20 Mar 1996 13:21:12 +0100 clasohm added warning and automatic deactivation of HTML generation if we cannot write
Mon, 18 Mar 1996 13:42:35 +0100 paulson New file containing search tacticals
Fri, 15 Mar 1996 18:47:05 +0100 paulson Now provides astar versions (thanks to Norbert Voelker)
Fri, 15 Mar 1996 18:43:33 +0100 paulson New safe_meson_tac proves some harder theorems
Fri, 15 Mar 1996 18:42:36 +0100 paulson New safe_meson_tac uses iterative deepening
Fri, 15 Mar 1996 18:41:04 +0100 paulson Sets a lower value of Unify.search_bound
Fri, 15 Mar 1996 18:39:08 +0100 paulson Search tacticals moved to search.ML
Fri, 15 Mar 1996 18:38:24 +0100 paulson Updated for new file search.ML
Fri, 15 Mar 1996 13:34:39 +0100 clasohm updated syntax of datatype declaration
Fri, 15 Mar 1996 12:01:19 +0100 berghofe Added some functions which allow redirection of Isabelle's output
Thu, 14 Mar 1996 16:40:18 +0100 paulson Functions moved to Pure/search.ML and classical.ML
Thu, 14 Mar 1996 12:21:07 +0100 clasohm updated syntax of datatype definitions: "C t1 ... tn" instead of "C(t1,...,tn)"
Thu, 14 Mar 1996 12:19:49 +0100 clasohm added @SMLdebug=/dev/null to supress GC messages
Thu, 14 Mar 1996 10:40:21 +0100 berghofe Added some optimized versions of functions dealing with sets
Wed, 13 Mar 1996 11:56:15 +0100 clasohm replaced rules by primrec section
Wed, 13 Mar 1996 11:55:25 +0100 clasohm modified primrec so it can be used in MiniML/Type.thy
Tue, 12 Mar 1996 14:39:34 +0100 clasohm added constdefs section
Tue, 12 Mar 1996 14:38:58 +0100 clasohm removed make_chart
Tue, 12 Mar 1996 12:59:56 +0100 regensbu added ' make_html:=false;' to end of ROOT file
Mon, 11 Mar 1996 23:59:22 +0100 clasohm added constdefs section
Mon, 11 Mar 1996 19:42:55 +0100 nipkow Non-matching congruence rule in rewriter is simply ignored.
Mon, 11 Mar 1996 14:19:12 +0100 paulson New theorem: Inter_Un_subset
Mon, 11 Mar 1996 14:18:06 +0100 paulson Now catches "by(" too
Mon, 11 Mar 1996 14:16:35 +0100 paulson name_thm: now keeps the previous deriviation!
Mon, 11 Mar 1996 14:13:36 +0100 paulson Made an exception handler more specific
Mon, 11 Mar 1996 14:09:50 +0100 paulson Deleted faulty comment; proved new rule Inter_Un_subset
Mon, 11 Mar 1996 14:08:09 +0100 paulson New, one-line proof of inj_Atom
Mon, 11 Mar 1996 14:05:45 +0100 paulson deleted obsolete comment
Mon, 11 Mar 1996 14:04:37 +0100 paulson set_cs now includes singleton_inject
Mon, 11 Mar 1996 14:03:30 +0100 paulson Added formulation of Halting Problem
Mon, 11 Mar 1996 11:49:05 +0100 clasohm added constdefs section
Fri, 08 Mar 1996 13:11:09 +0100 clasohm added constdefs section
Wed, 06 Mar 1996 14:19:39 +0100 clasohm added constdefs section
Wed, 06 Mar 1996 14:12:24 +0100 clasohm added constdefs section
Wed, 06 Mar 1996 14:11:41 +0100 clasohm added constdefs
Wed, 06 Mar 1996 14:10:44 +0100 clasohm moved part of delete_thms into init_thyinfo
Wed, 06 Mar 1996 13:57:07 +0100 paulson Ran expandshort
Wed, 06 Mar 1996 12:52:11 +0100 paulson Ran expandshort
Wed, 06 Mar 1996 12:19:16 +0100 clasohm documented new function 'section'
Wed, 06 Mar 1996 10:26:43 +0100 paulson EX_FILES includes new oracle examples, and uses the
Wed, 06 Mar 1996 10:14:47 +0100 paulson Now loads IffOracle, the oracles example
Wed, 06 Mar 1996 10:05:00 +0100 nipkow Added 'section' commands
Tue, 05 Mar 1996 17:37:28 +0100 paulson New documentation for example
Tue, 05 Mar 1996 17:29:58 +0100 paulson Changed HOL to ZF in title; added address
(0) -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip