2004-10-26 berghofe 2004-10-26 Changed function cabs to also allow abstraction over Vars.
2004-10-26 berghofe 2004-10-26 Added function merge_alists'.
2004-10-26 berghofe 2004-10-26 Added function strip_type (for ctyps).
2004-10-26 berghofe 2004-10-26 Added preprocessors.
2004-10-26 berghofe 2004-10-26 Added setup for code generator.
2004-10-26 berghofe 2004-10-26 Added simple code generator.
2004-10-26 berghofe 2004-10-26 Removed code generator stuff. Code generation is now handled by code generator in typedef_package.
2004-10-26 berghofe 2004-10-26 Added call to Codegen.preprocess.
2004-10-26 berghofe 2004-10-26 Fixed problem with sorts in function make_casedists.
2004-10-25 nipkow 2004-10-25 fixed urls
2004-10-24 aspinall 2004-10-24 Simplification to symbol processing; put quotes around theory name in message.
2004-10-21 aspinall 2004-10-21 Fix <closetheory>
2004-10-19 berghofe 2004-10-19 Replaced PolyML specific print function by Display.print_thm(s)
2004-10-19 paulson 2004-10-19 converted some induct_tac to induct
2004-10-18 dixon 2004-10-18 added a missing case (Var x) that made finding a case split fail, in order to prove the specification equation from the split versions, for some recursive functions.
2004-10-18 berghofe 2004-10-18 Replaced list of bound variables in simpset by maximal index of bound variables. This allows new variable names to be generated more quickly (without calling variant).
2004-10-15 schirmer 2004-10-15 record_split_simp_tac now can get simp rules as parameter
2004-10-15 nipkow 2004-10-15 update
2004-10-15 nipkow 2004-10-15 added and renamed
2004-10-14 nipkow 2004-10-14 Added a few lemmas
2004-10-13 nipkow 2004-10-13 mod becuase of chnage in induct
2004-10-12 nipkow 2004-10-12 Added solution to exercise.
2004-10-12 nipkow 2004-10-12 *** empty log message ***
2004-10-12 paulson 2004-10-12 tweaks concerned with poly bug-fixing
2004-10-11 berghofe 2004-10-11 Replaced the_context() by theory "Presburger" in call of invoke_oracle.
2004-10-11 berghofe 2004-10-11 Tuned some proofs.
2004-10-11 berghofe 2004-10-11 Added entry in Settings menu for Toplevel.skip_proofs flag.
2004-10-11 berghofe 2004-10-11 Some changes to allow skipping of proof scripts.
2004-10-11 nipkow 2004-10-11 Proofs needed to be updated because induction now preserves name of induction variable.
2004-10-11 nipkow 2004-10-11 Induction now preserves the name of the induction variable.
2004-10-07 paulson 2004-10-07 simplification tweaks for better arithmetic reasoning
2004-10-06 chaieb 2004-10-06 *** empty log message ***
2004-10-06 chaieb 2004-10-06 a very simple decision procedure for a fragment of bounded arithmetic
2004-10-06 chaieb 2004-10-06 changed in order to insert Barith.thy
2004-10-05 paulson 2004-10-05 auto update
2004-10-05 paulson 2004-10-05 new simprules for abs and for things like a/b<1
2004-10-04 paulson 2004-10-04 revised simprules for division
2004-10-04 paulson 2004-10-04 PDF_VIEWER suggestion
2004-10-04 paulson 2004-10-04 Abstract for the Isabelle system
2004-10-02 aspinall 2004-10-02 Add openblock/closeblock to other opengoal/closegoal elements
2004-10-01 aspinall 2004-10-01 Allow scanning to recover and reconstruct bad input
2004-10-01 paulson 2004-10-01 patch to "display"
2004-10-01 paulson 2004-10-01 display-drafts now uses pdf!
2004-10-01 paulson 2004-10-01 tweaking of arithmetic proofs
2004-10-01 aspinall 2004-10-01 Comments
2004-09-30 paulson 2004-09-30 tidied
2004-09-30 kleing 2004-09-30 display pdf as well as dvi
2004-09-30 schirmer 2004-09-30 bug-fix with new records
2004-09-29 aspinall 2004-09-29 Remove white space skipping in element content; XML specification clearly requires whitespace to be passed to application.
2004-09-29 schirmer 2004-09-29 tuned performance of record definition
2004-09-29 paulson 2004-09-29 tidying up; identifying the main theorems
2004-09-28 ballarin 2004-09-28 Changes in "includes".
2004-09-28 ballarin 2004-09-28 Bug fixes.
2004-09-28 aspinall 2004-09-28 Add text_charref to encode a string using character references
2004-09-28 aspinall 2004-09-28 Remove double escaping of backslash in PGML. Remove use of character refs in <whitespace>
2004-09-28 aspinall 2004-09-28 Fix to unparse to not double-escape backslash
2004-09-27 aspinall 2004-09-27 Add filenamextns to prover info. Update doc location. Add whitespace element in parseresult
2004-09-27 aspinall 2004-09-27 Add newline after CDATA for sake of HaXml
2004-09-27 ballarin 2004-09-27 Modified locales: improved implementation of "includes".
2004-09-23 paulson 2004-09-23 some x-symbols