2001-09-27 |
wenzelm |
ex/Hilbert_Classical.thy ex/document/root.tex;
|
file |
diff |
annotate
|
2001-08-31 |
wenzelm |
HOL-Real-Hyperreal made a plain session (no longer an image);
|
file |
diff |
annotate
|
2001-08-31 |
berghofe |
Added new files for code generator.
|
file |
diff |
annotate
|
2001-07-25 |
paulson |
partial restructuring to reduce dependence on Axiom of Choice
|
file |
diff |
annotate
|
2001-07-23 |
paulson |
new GroupTheory examples; PiSets moved to GroupTheory, while LocaleGroup deleted
|
file |
diff |
annotate
|
2001-07-03 |
wenzelm |
Library/ROOT.ML moved to Library/Library/ROOT.ML to avoid accidential
|
file |
diff |
annotate
|
2001-07-03 |
paulson |
Locale-based group theory proofs
|
file |
diff |
annotate
|
2001-06-16 |
oheimb |
added NanoJava
|
file |
diff |
annotate
|
2001-06-10 |
paulson |
new GroupTheory example, e.g. the Sylow theorem (preliminary version)
|
file |
diff |
annotate
|
2001-06-09 |
paulson |
moved Primes.thy from NumberTheory to Library
|
file |
diff |
annotate
|
2001-06-08 |
nipkow |
Removed BCV
|
file |
diff |
annotate
|
2001-05-31 |
wenzelm |
added HOL-CTL;
|
file |
diff |
annotate
|
2001-05-31 |
oheimb |
added Library/Nat_Infinity.thy and Library/Continuity.thy
|
file |
diff |
annotate
|
2001-05-08 |
paulson |
conversion of Auth/TLS to Isar script
|
file |
diff |
annotate
|
2001-04-24 |
paulson |
(rough) conversion of Auth/Recur to Isar format
|
file |
diff |
annotate
|
2001-04-12 |
paulson |
converted many HOL/Auth theories to Isar scripts
|
file |
diff |
annotate
|
2001-03-28 |
nipkow |
MicroJava/BV dependencies incomplete
|
file |
diff |
annotate
|
2001-03-23 |
nipkow |
added one point simprocs for bounded quantifiers
|
file |
diff |
annotate
|
2001-03-05 |
paulson |
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
|
file |
diff |
annotate
|
2001-03-02 |
paulson |
conversion of Message.thy to Isar format
|
file |
diff |
annotate
|
2001-02-15 |
oheimb |
Ord.thy/.ML converted to Isar
|
file |
diff |
annotate
|
2001-02-13 |
paulson |
partial conversion to Isar script style in HOL/Auth removes some .ML files
|
file |
diff |
annotate
|
2001-02-09 |
kleing |
removed MicroJava/Digest.thy
|
file |
diff |
annotate
|
2001-02-04 |
wenzelm |
HOL-NumberTheory: converted to new-style format and proper document setup;
|
file |
diff |
annotate
|
2001-02-03 |
wenzelm |
Induct: converted some theories to new-style format;
|
file |
diff |
annotate
|
2001-02-01 |
oheimb |
converted to Isar, simplifying recursion on class hierarchy
|
file |
diff |
annotate
|
2001-02-01 |
wenzelm |
converted to new-style theories;
|
file |
diff |
annotate
|
2001-01-28 |
nipkow |
fixed set comprehension print translation
|
file |
diff |
annotate
|
2001-01-25 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
2001-01-25 |
wenzelm |
Transitive_Closure turned into new-style theory;
|
file |
diff |
annotate
|
2001-01-23 |
wenzelm |
added HOL-Unix example;
|
file |
diff |
annotate
|
2001-01-19 |
wenzelm |
added Library/Ring_and_Field_Example.thy;
|
file |
diff |
annotate
|
2001-01-19 |
wenzelm |
added HOL/Library/Nested_Environment.thy;
|
file |
diff |
annotate
|
2001-01-16 |
kleing |
removed obsolete MicroJava/JVM/Store.thy
|
file |
diff |
annotate
|
2001-01-15 |
wenzelm |
removed ex/StringEx.ML;
|
file |
diff |
annotate
|
2001-01-12 |
wenzelm |
added Induct/Sigma_Algebra.thy;
|
file |
diff |
annotate
|
2001-01-07 |
wenzelm |
removed MicroJava/BV/Convert.thy;
|
file |
diff |
annotate
|
2001-01-05 |
paulson |
new UNITY examples by Sidi Ehmety
|
file |
diff |
annotate
|
2001-01-03 |
wenzelm |
TFL: renamed .sml to .ML;
|
file |
diff |
annotate
|
2001-01-01 |
paulson |
put in some missing Hyperreal files
|
file |
diff |
annotate
|
2000-12-30 |
paulson |
separation of HOL-Hyperreal from HOL-Real
|
file |
diff |
annotate
|
2000-12-23 |
wenzelm |
Tools/string_syntax.ML;
|
file |
diff |
annotate
|
2000-12-21 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
2000-12-19 |
paulson |
new file extract_common_term.ML for the cancel-factor simprocs
|
file |
diff |
annotate
|
2000-12-16 |
wenzelm |
tuned HOL/Real/HahnBanach;
|
file |
diff |
annotate
|
2000-12-06 |
wenzelm |
added Library/Rational_Numbers.thy;
|
file |
diff |
annotate
|
2000-12-01 |
nipkow |
Linear arithmetic now copes with mixed nat/int formulae.
|
file |
diff |
annotate
|
2000-11-29 |
paulson |
new simproc file cancel_numeral_factor.ML
|
file |
diff |
annotate
|
2000-11-17 |
wenzelm |
Library/Ring_and_Field.thy;
|
file |
diff |
annotate
|
2000-11-10 |
wenzelm |
proper theory context for mesontest2;
|
file |
diff |
annotate
|
2000-10-30 |
wenzelm |
added ex/PER.thy;
|
file |
diff |
annotate
|
2000-10-26 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
2000-10-25 |
wenzelm |
"List prefixes" library theory (replaces old Lex/Prefix);
|
file |
diff |
annotate
|
2000-10-19 |
wenzelm |
added Tools/induct_attrib.ML;
|
file |
diff |
annotate
|
2000-10-18 |
wenzelm |
removed Library/Accessible_Part.ML;
|
file |
diff |
annotate
|
2000-10-18 |
wenzelm |
added HOL/Library, rearranged several files;
|
file |
diff |
annotate
|
2000-10-13 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
2000-10-12 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
2000-10-05 |
wenzelm |
* HOL/Lattice: fundamental concepts of lattice theory and order structures;
|
file |
diff |
annotate
|
2000-10-03 |
wenzelm |
added Isar_examples/Hoare.thy Isar_examples/HoareEx.thy;
|
file |
diff |
annotate
|