isabelle: Graph

Mercurial Mercurial > repos > isabelle / graph

summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
less more | (0) -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

Examples call gocls to make goal clauses
1996-03-21, by paulson
Now labels the Horn and goal clauses to make the proof
1996-03-21, by paulson
For the new version of name_thm. Now the same theorem
1996-03-21, by paulson
name_thm no longer takes a theory argument, as the
1996-03-21, by paulson
Printing & string functions moved to display.ML
1996-03-21, by paulson
Now loads deriv.ML
1996-03-21, by paulson
Includes deriv.ML and display.ML as dependencies
1996-03-20, by paulson
New module for proof objects (deriviations)
1996-03-20, by paulson
maketest now closes the output file
1996-03-20, by paulson
New module for display/printing operations, taken from drule.ML
1996-03-20, by paulson
Describes proof objects and Deriv module
1996-03-20, by paulson
added warning and automatic deactivation of HTML generation if we cannot write
1996-03-20, by clasohm
New file containing search tacticals
1996-03-18, by paulson
Now provides astar versions (thanks to Norbert Voelker)
1996-03-15, by paulson
New safe_meson_tac proves some harder theorems
1996-03-15, by paulson
New safe_meson_tac uses iterative deepening
1996-03-15, by paulson
Sets a lower value of Unify.search_bound
1996-03-15, by paulson
Search tacticals moved to search.ML
1996-03-15, by paulson
Updated for new file search.ML
1996-03-15, by paulson
updated syntax of datatype declaration
1996-03-15, by clasohm
Added some functions which allow redirection of Isabelle's output
1996-03-15, by berghofe
Functions moved to Pure/search.ML and classical.ML
1996-03-14, by paulson
updated syntax of datatype definitions: "C t1 ... tn" instead of "C(t1,...,tn)"
1996-03-14, by clasohm
added @SMLdebug=/dev/null to supress GC messages
1996-03-14, by clasohm
Added some optimized versions of functions dealing with sets
1996-03-14, by berghofe
replaced rules by primrec section
1996-03-13, by clasohm
modified primrec so it can be used in MiniML/Type.thy
1996-03-13, by clasohm
added constdefs section
1996-03-12, by clasohm
removed make_chart
1996-03-12, by clasohm
added ' make_html:=false;' to end of ROOT file
1996-03-12, by regensbu
added constdefs section
1996-03-11, by clasohm
Non-matching congruence rule in rewriter is simply ignored.
1996-03-11, by nipkow
New theorem: Inter_Un_subset
1996-03-11, by paulson
Now catches "by(" too
1996-03-11, by paulson
name_thm: now keeps the previous deriviation!
1996-03-11, by paulson
Made an exception handler more specific
1996-03-11, by paulson
Deleted faulty comment; proved new rule Inter_Un_subset
1996-03-11, by paulson
New, one-line proof of inj_Atom
1996-03-11, by paulson
deleted obsolete comment
1996-03-11, by paulson
set_cs now includes singleton_inject
1996-03-11, by paulson
Added formulation of Halting Problem
1996-03-11, by paulson
added constdefs section
1996-03-11, by clasohm
added constdefs section
1996-03-08, by clasohm
added constdefs section
1996-03-06, by clasohm
added constdefs section
1996-03-06, by clasohm
added constdefs
1996-03-06, by clasohm
moved part of delete_thms into init_thyinfo
1996-03-06, by clasohm
Ran expandshort
1996-03-06, by paulson
Ran expandshort
1996-03-06, by paulson
documented new function 'section'
1996-03-06, by clasohm
EX_FILES includes new oracle examples, and uses the
1996-03-06, by paulson
Now loads IffOracle, the oracles example
1996-03-06, by paulson
Added 'section' commands
1996-03-06, by nipkow
New documentation for example
1996-03-05, by paulson
Changed HOL to ZF in title; added address
1996-03-05, by paulson
New documentation for example
1996-03-05, by paulson
Corrected URL
1996-03-05, by paulson
New documentation for examples
1996-03-05, by paulson
Put quotes around URLs in links
1996-03-05, by paulson
Put quotes around URLs in links
1996-03-05, by paulson

less more | (0) -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip

isabelle