2005-02-09 nipkow 2005-02-09 added lattice_locales
2005-02-09 nipkow 2005-02-09 Extracted generic lattice stuff to new Lattice_Locales.thy
2005-02-09 nipkow 2005-02-09 New
2005-02-09 paulson 2005-02-09 new foldSet proofs
2005-02-09 paulson 2005-02-09 revised fold1 proofs
2005-02-09 paulson 2005-02-09 revised fold1 proofs
2005-02-08 nipkow 2005-02-08 cvs merge problem fixed
2005-02-08 paulson 2005-02-08 new treatment of fold1
2005-02-08 nipkow 2005-02-08 Fixed lattice defns
2005-02-07 nipkow 2005-02-07 *** empty log message ***
2005-02-07 nipkow 2005-02-07 fixed latex problems by including bigsqcap
2005-02-07 nipkow 2005-02-07 fixed latex problems
2005-02-06 paulson 2005-02-06 fixed mac line
2005-02-05 nipkow 2005-02-05 Added Lattice locale
2005-02-04 paulson 2005-02-04 clausification and proof reconstruction
2005-02-04 paulson 2005-02-04 comment
2005-02-04 nipkow 2005-02-04 Added semi-lattice locales and reorganized fold1 lemmas
2005-02-03 nipkow 2005-02-03 added find_rewrites
2005-02-03 paulson 2005-02-03 new treatment of demodulation in proof reconstruction
2005-02-03 kleing 2005-02-03 don't generate latex for LaTeXsugar and OptionalSugar
2005-02-03 kleing 2005-02-03 removed sugar.sty (obsolete for devel version)
2005-02-03 kleing 2005-02-03 not needed any more by LaTeXSugar
2005-02-03 kleing 2005-02-03 Document now applies to devel version (and Isabelle 2005)
2005-02-02 berghofe 2005-02-02 Replaced application of subst by simplesubst in proof of app_Var_NF to avoid problems with program extraction.
2005-02-02 berghofe 2005-02-02 Replaced application of subst by simplesubst in proof of rev_induct to avoid problems with program extraction.
2005-02-02 paulson 2005-02-02 tidying of some subst/simplesubst proofs
2005-02-02 paulson 2005-02-02 generalization and tidying
2005-02-02 paulson 2005-02-02 improved handling of chained facts
2005-02-02 nipkow 2005-02-02 Max_le -> Max_ge
2005-02-02 nipkow 2005-02-02 fold and fol1 changes
2005-02-02 nipkow 2005-02-02 added [simp]
2005-02-02 kleing 2005-02-02 link to PG FAQ for start up problem
2005-02-01 paulson 2005-02-01 the new subst tactic, by Lucas Dixon
2005-01-30 nipkow 2005-01-30 renamed a few vars, added a lemma
2005-01-28 nipkow 2005-01-28 proof simpification
2005-01-28 kleing 2005-01-28 moved sugar.sty to textinputs
2005-01-28 kleing 2005-01-28 -H false for showing proofs (not -H true)
2005-01-27 nipkow 2005-01-27 fixed bugs
2005-01-27 berghofe 2005-01-27 - Proofs are now hidden by default when generating documents - New syntax for referring to theorems in lists - Improvements to theory loader (relative and absolute paths)
2005-01-27 berghofe 2005-01-27 Proofs are now hidden by default.
2005-01-27 berghofe 2005-01-27 - Proofs are now hidden by default - Added show_var_qmarks flag
2005-01-27 berghofe 2005-01-27 Added show_var_qmarks flag.
2005-01-26 nipkow 2005-01-26 *** empty log message ***
2005-01-26 nipkow 2005-01-26 added OptionalSugar
2005-01-26 nipkow 2005-01-26 new
2005-01-26 nipkow 2005-01-26 moved to HOL/Library
2005-01-26 nipkow 2005-01-26 *** empty log message ***
2005-01-26 paulson 2005-01-26 implemented cache for conversion to clauses
2005-01-25 nipkow 2005-01-25 enclosed in (*<*) (*>*)
2005-01-24 berghofe 2005-01-24 Added variant of eres_inst_tac that operates on indexnames instead of strings.
2005-01-24 berghofe 2005-01-24 Adapted to modified interface of PureThy.get_thm(s).
2005-01-24 berghofe 2005-01-24 Eliminated hack for deleting leading question mark from induction variable name.
2005-01-24 berghofe 2005-01-24 Replaced xstring by thmref.
2005-01-24 berghofe 2005-01-24 Removed unnecessary subsignature checks to speed up rewriting.
2005-01-24 berghofe 2005-01-24 Introduced function DatatypeProp.make_primrec_Ts to avoid code duplication.
2005-01-24 berghofe 2005-01-24 Replaced xstring by thmref.
2005-01-24 berghofe 2005-01-24 Adapted to modified interface of PureThy.get_thm(s).
2005-01-24 berghofe 2005-01-24 Specific theorems in a named list of theorems can now be referred to via indices (type thmref).
2005-01-24 paulson 2005-01-24 updated description of arith_tac
2005-01-24 paulson 2005-01-24 thin_tac now works on P==>Q