| 2009-04-27 |
haftmann |
cleaned up theory power further
|
file |
diff |
annotate
|
| 2009-04-24 |
haftmann |
funpow and relpow with shared "^^" syntax
|
file |
diff |
annotate
|
| 2009-04-22 |
haftmann |
dropped duplication
|
file |
diff |
annotate
|
| 2009-04-22 |
haftmann |
code_datatype and power
|
file |
diff |
annotate
|
| 2009-04-20 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2009-04-20 |
haftmann |
changes in power operations
|
file |
diff |
annotate
|
| 2009-04-17 |
haftmann |
formal declaration of undefined parameters after class instantiation
|
file |
diff |
annotate
|
| 2009-04-17 |
haftmann |
separated funpow, relpow from power on monoids
|
file |
diff |
annotate
|
| 2009-04-16 |
haftmann |
tightended specification of class semiring_div
|
file |
diff |
annotate
|
| 2009-04-20 |
wenzelm |
back to non-release mode;
|
file |
diff |
annotate
|
| 2009-04-02 |
wenzelm |
some more HOL-Nominal news;
|
file |
diff |
annotate
|
| 2009-04-02 |
wenzelm |
some HOL-Nominal news;
|
file |
diff |
annotate
|
| 2009-04-02 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2009-04-02 |
wenzelm |
misc cleanup and rearrangements for Isabelle2009 release;
|
file |
diff |
annotate
|
| 2009-03-27 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2009-03-27 |
haftmann |
dropped toy example Code_Antiq
|
file |
diff |
annotate
|
| 2009-03-26 |
wenzelm |
interpretation/interpret: prefixes are mandatory by default;
|
file |
diff |
annotate
|
| 2009-03-24 |
nipkow |
NEWS: [arith]
|
file |
diff |
annotate
|
| 2009-03-20 |
wenzelm |
Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
|
file |
diff |
annotate
|
| 2009-03-19 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2009-03-16 |
huffman |
document new additions to HOL/Library
|
file |
diff |
annotate
|
| 2009-03-16 |
wenzelm |
simplifief 'method_setup' command;
|
file |
diff |
annotate
|
| 2009-03-15 |
wenzelm |
merged
|
file |
diff |
annotate
|
| 2009-03-14 |
immler |
updated NEWS
|
file |
diff |
annotate
|
| 2009-03-15 |
wenzelm |
simplified attribute and method setup;
|
file |
diff |
annotate
|
| 2009-03-11 |
wenzelm |
added 'local_setup' command;
|
file |
diff |
annotate
|
| 2009-03-11 |
hoelzl |
Updated paths in Decision_Procs comments and NEWS
|
file |
diff |
annotate
|
| 2009-03-10 |
webertj |
Instead of giving up entirely, arith now ignores all inequalities when there are too many.
|
file |
diff |
annotate
|
| 2009-03-09 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 2009-03-09 |
wenzelm |
* More systematic treatment of long names, abstract name bindings, and name space operations.
|
file |
diff |
annotate
|
| 2009-03-06 |
haftmann |
constructive version of Cantor's first diagonalization argument
|
file |
diff |
annotate
|
| 2009-03-06 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2009-03-05 |
haftmann |
merged
|
file |
diff |
annotate
|
| 2009-03-05 |
haftmann |
set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
|
file |
diff |
annotate
|
| 2009-03-06 |
haftmann |
corrected slip in NEWS
|
file |
diff |
annotate
|
| 2009-03-06 |
haftmann |
added strict_mono predicate
|
file |
diff |
annotate
|
| 2009-03-05 |
huffman |
declare power_Suc [simp]; remove redundant type-specific versions of power_Suc
|
file |
diff |
annotate
|
| 2009-03-04 |
wenzelm |
NEWS: renamed o2s to Option.set;
|
file |
diff |
annotate
|
| 2009-03-04 |
nipkow |
Made Option a separate theory and renamed option_map to Option.map
|
file |
diff |
annotate
|
| 2009-03-03 |
nipkow |
removed and renamed redundant lemmas
|
file |
diff |
annotate
|
| 2009-03-02 |
nipkow |
name fix
|
file |
diff |
annotate
|
| 2009-03-02 |
nipkow |
name changes
|
file |
diff |
annotate
|
| 2009-03-01 |
nipkow |
removed redundant lemmas
|
file |
diff |
annotate
|
| 2009-02-28 |
huffman |
add news for HOLCF; fixed some typos and inaccuracies
|
file |
diff |
annotate
|
| 2009-02-28 |
wenzelm |
* New prover for coherent logic (see src/Tools/coherent.ML).
|
file |
diff |
annotate
|
| 2009-02-26 |
wenzelm |
tuned NEWS;
|
file |
diff |
annotate
|
| 2009-02-25 |
nipkow |
NEWS
|
file |
diff |
annotate
|
| 2009-02-21 |
nipkow |
NEWS
|
file |
diff |
annotate
|
| 2009-02-12 |
kleing |
added find_consts to NEWS and CONTRIBUTORS
|
file |
diff |
annotate
|
| 2009-02-11 |
kleing |
fixed typo
|
file |
diff |
annotate
|
| 2009-02-11 |
kleing |
updated NEWS etc with "solves" criterion and auto_solves
|
file |
diff |
annotate
|
| 2009-02-06 |
haftmann |
session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there
|
file |
diff |
annotate
|
| 2009-02-05 |
hoelzl |
Updated NEWS about approximation
|
file |
diff |
annotate
|
| 2009-02-05 |
hoelzl |
Add approximation method
|
file |
diff |
annotate
|
| 2009-02-03 |
haftmann |
handling type classes without parameters
|
file |
diff |
annotate
|
| 2009-02-03 |
haftmann |
established session HOL-Reflection
|
file |
diff |
annotate
|
| 2009-01-28 |
nipkow |
-
|
file |
diff |
annotate
|
| 2009-01-28 |
haftmann |
Reflection.thy now in HOL/Library
|
file |
diff |
annotate
|
| 2009-01-26 |
haftmann |
entry point for Word library now named Word
|
file |
diff |
annotate
|
| 2009-01-22 |
haftmann |
binding replaces Binding.T
|
file |
diff |
annotate
|