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