1996-03-20 paulson 1996-03-20 New module for proof objects (deriviations)
1996-03-20 paulson 1996-03-20 maketest now closes the output file Declared type mtree for proof objects
1996-03-20 paulson 1996-03-20 New module for display/printing operations, taken from drule.ML
1996-03-20 paulson 1996-03-20 Describes proof objects and Deriv module
1996-03-20 clasohm 1996-03-20 added warning and automatic deactivation of HTML generation if we cannot write .theory_list.txt; fixed bug which occured when index_path's value is "/"
1996-03-18 paulson 1996-03-18 New file containing search tacticals
1996-03-15 paulson 1996-03-15 Now provides astar versions (thanks to Norbert Voelker)
1996-03-15 paulson 1996-03-15 New safe_meson_tac proves some harder theorems
1996-03-15 paulson 1996-03-15 New safe_meson_tac uses iterative deepening
1996-03-15 paulson 1996-03-15 Sets a lower value of Unify.search_bound
1996-03-15 paulson 1996-03-15 Search tacticals moved to search.ML
1996-03-15 paulson 1996-03-15 Updated for new file search.ML
1996-03-15 clasohm 1996-03-15 updated syntax of datatype declaration
1996-03-15 berghofe 1996-03-15 Added some functions which allow redirection of Isabelle's output
1996-03-14 paulson 1996-03-14 Functions moved to Pure/search.ML and classical.ML
1996-03-14 clasohm 1996-03-14 updated syntax of datatype definitions: "C t1 ... tn" instead of "C(t1,...,tn)"
1996-03-14 clasohm 1996-03-14 added @SMLdebug=/dev/null to supress GC messages
1996-03-14 berghofe 1996-03-14 Added some optimized versions of functions dealing with sets (i.e. mem, ins, eq_set etc.) which do not use the polymorphic = operator
1996-03-13 clasohm 1996-03-13 replaced rules by primrec section
1996-03-13 clasohm 1996-03-13 modified primrec so it can be used in MiniML/Type.thy
1996-03-12 clasohm 1996-03-12 added constdefs section
1996-03-12 clasohm 1996-03-12 removed make_chart
1996-03-12 regensbu 1996-03-12 added ' make_html:=false;' to end of ROOT file
1996-03-11 clasohm 1996-03-11 added constdefs section
1996-03-11 nipkow 1996-03-11 Non-matching congruence rule in rewriter is simply ignored. Used to cause error message.
1996-03-11 paulson 1996-03-11 New theorem: Inter_Un_subset
1996-03-11 paulson 1996-03-11 Now catches "by(" too
1996-03-11 paulson 1996-03-11 name_thm: now keeps the previous deriviation!
1996-03-11 paulson 1996-03-11 Made an exception handler more specific
1996-03-11 paulson 1996-03-11 Deleted faulty comment; proved new rule Inter_Un_subset
1996-03-11 paulson 1996-03-11 New, one-line proof of inj_Atom
1996-03-11 paulson 1996-03-11 deleted obsolete comment
1996-03-11 paulson 1996-03-11 set_cs now includes singleton_inject
1996-03-11 paulson 1996-03-11 Added formulation of Halting Problem
1996-03-11 clasohm 1996-03-11 added constdefs section
1996-03-08 clasohm 1996-03-08 added constdefs section
1996-03-06 clasohm 1996-03-06 added constdefs section
1996-03-06 clasohm 1996-03-06 added constdefs section
1996-03-06 clasohm 1996-03-06 added constdefs
1996-03-06 clasohm 1996-03-06 moved part of delete_thms into init_thyinfo
1996-03-06 paulson 1996-03-06 Ran expandshort
1996-03-06 paulson 1996-03-06 Ran expandshort
1996-03-06 clasohm 1996-03-06 documented new function 'section'
1996-03-06 paulson 1996-03-06 EX_FILES includes new oracle examples, and uses the standard abbreviation convention.
1996-03-06 paulson 1996-03-06 Now loads IffOracle, the oracles example
1996-03-06 nipkow 1996-03-06 Added 'section' commands
1996-03-05 paulson 1996-03-05 New documentation for example
1996-03-05 paulson 1996-03-05 Changed HOL to ZF in title; added address
1996-03-05 paulson 1996-03-05 New documentation for example
1996-03-05 paulson 1996-03-05 Corrected URL
1996-03-05 paulson 1996-03-05 New documentation for examples
1996-03-05 paulson 1996-03-05 Put quotes around URLs in links
1996-03-05 paulson 1996-03-05 Put quotes around URLs in links
1996-03-05 paulson 1996-03-05 Converted TABs to spaces
1996-03-05 paulson 1996-03-05 Addition of oracles
1996-03-05 clasohm 1996-03-05 added function "section" for HTML section headings
1996-03-05 paulson 1996-03-05 Example of declaring oracles
1996-03-05 paulson 1996-03-05 More up-to-date references
1996-03-05 paulson 1996-03-05 Fuller and more up-to-date references
1996-03-05 paulson 1996-03-05 A mere adjustment of spacing