2012-04-20 huffman 2012-04-20 add transfer rule for 'id'
2012-04-20 huffman 2012-04-20 add new transfer rules and setup for lifting package
2012-04-20 huffman 2012-04-20 setup_lifting preprocesses forall_transfer rule by unfolding mem_Collect_eq
2012-04-20 hoelzl 2012-04-20 NEWS
2012-04-20 hoelzl 2012-04-20 hide code generation facts in the Float theory, they are only exported for Approximation
2012-04-20 nipkow 2012-04-20 merged
2012-04-20 nipkow 2012-04-20 forgot to add file
2012-04-20 huffman 2012-04-20 make correspondence tactic more robust by replacing lhs with schematic variable before applying intro rules
2012-04-19 wenzelm 2012-04-19 merged
2012-04-19 hoelzl 2012-04-19 NEWS
2012-04-19 hoelzl 2012-04-19 transfer now handles Let
2012-04-19 nipkow 2012-04-19 merged
2012-04-19 nipkow 2012-04-19 added revised version of Abs_Int
2012-04-19 huffman 2012-04-19 add transfer rule for Let
2012-04-19 huffman 2012-04-19 add code lemmas for word operations
2012-04-19 haftmann 2012-04-19 tuned whitespace
2012-04-19 haftmann 2012-04-19 dropped dead code
2012-04-19 kuncar 2012-04-19 rename no_code to no_abs_code - more appropriate name
2012-04-19 kuncar 2012-04-19 use tnames for bound variables in rsp thms
2012-04-19 blanchet 2012-04-19 true delayed evaluation of "SPASS_VERSION" environment variable
2012-04-19 blanchet 2012-04-19 merged
2012-04-19 blanchet 2012-04-19 use latest Z3
2012-04-19 nipkow 2012-04-19 merged
2012-04-19 nipkow 2012-04-19 reorganised IMP
2012-04-19 hoelzl 2012-04-19 use real :: float => real as lifting-morphism so we can directlry use the rep_eq theorems
2012-04-18 hoelzl 2012-04-18 use lifting to introduce floating point numbers
2012-04-18 hoelzl 2012-04-18 replace the float datatype by a type with unique representation
2012-04-18 hoelzl 2012-04-18 add lemmas to remove real conversions when compared to power of numerals
2012-04-18 hoelzl 2012-04-18 add simp rules to rewrite comparisons of 1 and real
2012-04-18 hoelzl 2012-04-18 add lemma to equate floor and div
2012-04-18 hoelzl 2012-04-18 add powr_inj
2012-04-18 hoelzl 2012-04-18 add lemmas to rewrite powr to power
2012-04-18 hoelzl 2012-04-18 add lemmas to compare log with 0 and 1
2012-04-18 hoelzl 2012-04-18 add ceiling_diff_floor_le_1
2012-04-19 wenzelm 2012-04-19 display Java 7 only code for now (cf. b9e2ed4b1579);
2012-04-19 wenzelm 2012-04-19 some sidekick options for more advanced completion;
2012-04-19 wenzelm 2012-04-19 custom ListCellRenderer with text area font ensures that symbols are displayed reliably;
2012-04-19 wenzelm 2012-04-19 tuned imports;
2012-04-19 wenzelm 2012-04-19 more robust wrt. exceptions;
2012-04-19 wenzelm 2012-04-19 accomodate digits within Isar command names, notably 'try0';
2012-04-19 wenzelm 2012-04-19 more robust Sledgehammer in Prover IDE;
2012-04-19 wenzelm 2012-04-19 test with jdk-7u3 that is also bundled;
2012-04-19 kuncar 2012-04-19 create thm names correctly
2012-04-19 wenzelm 2012-04-19 updated components according to tentative bundle;
2012-04-19 wenzelm 2012-04-19 back to isatest with official polyml-5.4.1 (cf. ffa6e10df091);
2012-04-19 huffman 2012-04-19 use simpler method for preserving bound variable names in transfer tactic
2012-04-19 huffman 2012-04-19 tuned lemmas (v)image_id; removed duplicate of vimage_id
2012-04-19 blanchet 2012-04-19 use latest SPASS
2012-04-19 blanchet 2012-04-19 doc update
2012-04-19 haftmann 2012-04-19 dropped dead code; tuned
2012-04-19 huffman 2012-04-19 generate abs_induct rules for quotient types
2012-04-19 haftmann 2012-04-19 tuned
2012-04-19 haftmann 2012-04-19 corrected Nbe.static_value: ignore cached compilations; tuned
2012-04-19 haftmann 2012-04-19 tuned heading
2012-04-18 haftmann 2012-04-18 tuned name
2012-04-19 sultana 2012-04-19 improved threading of thy-values through interpret functions;
2012-04-19 sultana 2012-04-19 exceptions related to interpreting tptp problems now mention the relevant position in the tptp file;
2012-04-18 huffman 2012-04-18 add option to transfer method for specifying variables not to generalize over
2012-04-17 Thomas Sewell 2012-04-17 New tactic "word_bitwise" expands word equalities/inequalities into logic.
2012-04-18 kuncar 2012-04-18 setup_lifting: no_code switch and supoport for quotient theorems