2013-12-27 haftmann 2013-12-27 prefer target-style syntaxx for sublocale
2013-12-26 haftmann 2013-12-26 prefer ephemeral interpretation over interpretation in proof contexts; prefer context begin ... end blocks for often-occuring assumptions; slightly more complete interpretations into abstract algebraic structures for gcd/lcm
2013-12-25 haftmann 2013-12-25 self-contained formulation of subclass command, avoiding hard-wired Named_Target.init
2013-12-25 haftmann 2013-12-25 ephemeral interpretation also formally works on theory level
2013-12-25 haftmann 2013-12-25 abolished slightly odd global lattice interpretation for min/max
2013-12-25 haftmann 2013-12-25 prefer more canonical names for lemmas on min/max
2013-12-25 haftmann 2013-12-25 explicit distributivity facts on min/max
2013-12-25 haftmann 2013-12-25 postponed min/max lemmas until abstract lattice is available
2013-12-25 haftmann 2013-12-25 tuned structure of min/max lemmas
2013-12-25 haftmann 2013-12-25 prefer abstract simp rule
2013-12-25 haftmann 2013-12-25 more lemmas on abstract lattices
2013-12-24 haftmann 2013-12-24 tuning and augmentation of min/max lemmas; more lemmas and simp rules for abstract lattices with order; tuned proofs
2013-12-24 haftmann 2013-12-24 more general induction rule; tuned proofs
2013-12-23 haftmann 2013-12-23 convenient printing of polynomial values
2013-12-23 haftmann 2013-12-23 prefer "Bits" as theory name for abstract bit operations, similar to "Orderings", "Lattices", "Groups" etc.
2013-12-23 haftmann 2013-12-23 prefer Y_of_X over X_to_Y; prefer alist over assoc_list; prefer explicit prefix
2013-12-23 panny 2013-12-23 merge
2013-12-23 panny 2013-12-23 prevent ambiguity when mutual recursion maps a datatype to itself, which yielded wrong definitions in some cases (e.g. nat)
2013-12-23 haftmann 2013-12-23 NEWS
2013-12-23 haftmann 2013-12-23 dropped redundant lemma
2013-12-23 haftmann 2013-12-23 syntactically tuned
2013-12-23 haftmann 2013-12-23 prefer plain bool over dedicated type for binary digits
2013-12-23 nipkow 2013-12-23 tuned
2013-12-21 blanchet 2013-12-21 compile + reduce problem size by a notch
2013-12-21 blanchet 2013-12-21 generate exhaust from nchotomy
2013-12-21 blanchet 2013-12-21 made tactic work with theorems with multiple assumptions
2013-12-21 blanchet 2013-12-21 renamed 'exhaust' to 'nchotomy' since it's expressed in the object logic (cf. datatype package)
2013-12-18 traytel 2013-12-18 express weak pullback property of bnfs only in terms of the relator
2013-12-20 nipkow 2013-12-20 merged
2013-12-20 nipkow 2013-12-20 tuned
2013-12-20 blanchet 2013-12-20 reconstruct SPASS-Pirate steps of the form 'x ~= C x' (or more complicated)
2013-12-20 blanchet 2013-12-20 tuning whitespace
2013-12-20 blanchet 2013-12-20 recognize datatype reasoning in SPASS-Pirate
2013-12-20 blanchet 2013-12-20 note manually proved exclusiveness property
2013-12-20 blanchet 2013-12-20 note exhaust proof obligation
2013-12-20 blanchet 2013-12-20 compile
2013-12-19 blanchet 2013-12-19 implemented 'exhaustive' option in tactic
2013-12-19 blanchet 2013-12-19 tuning
2013-12-19 blanchet 2013-12-19 tuning
2013-12-19 blanchet 2013-12-19 tuning 'case' expressions
2013-12-19 blanchet 2013-12-19 don't do 'isar_try0' if preplaying is off
2013-12-19 blanchet 2013-12-19 more data structure refactoring
2013-12-19 blanchet 2013-12-19 data structure rationalization
2013-12-19 blanchet 2013-12-19 tuning
2013-12-19 blanchet 2013-12-19 refactored preplaying outcome data structure
2013-12-19 blanchet 2013-12-19 distinguish not preplayed & timed out
2013-12-19 blanchet 2013-12-19 pick up tfree/tvar type from SPASS-Pirate proof
2013-12-19 blanchet 2013-12-19 tuning
2013-12-19 blanchet 2013-12-19 extended ATP types with sorts
2013-12-19 blanchet 2013-12-19 removed debugging output
2013-12-19 blanchet 2013-12-19 honor SPASS-Pirate type arguments
2013-12-19 blanchet 2013-12-19 made SML/NJ-friendlier (hopefully)
2013-12-19 blanchet 2013-12-19 made timeouts in Sledgehammer not be 'option's -- simplified lots of code
2013-12-19 blanchet 2013-12-19 simplified data structure
2013-12-19 blanchet 2013-12-19 prevent curl's output to interfere with the prover's output
2013-12-19 blanchet 2013-12-19 tuning
2013-12-18 blanchet 2013-12-18 merge
2013-12-18 blanchet 2013-12-18 parse SPASS-Pirate types
2013-12-18 nipkow 2013-12-18 merged
2013-12-18 nipkow 2013-12-18 added lemma