| 2008-06-12 |
urbanc |
added CK_Machine to the nominal section
|
file |
diff |
annotate
|
| 2008-06-10 |
wenzelm |
added HOL/Tools/induct_tacs.ML;
|
file |
diff |
annotate
|
| 2008-06-10 |
haftmann |
major refactorings in code generator modules
|
file |
diff |
annotate
|
| 2008-06-01 |
urbanc |
new example
|
file |
diff |
annotate
|
| 2008-05-13 |
krauss |
fixed makefile
|
file |
diff |
annotate
|
| 2008-04-25 |
krauss |
Merged theories about wellfoundedness into one: Wellfounded.thy
|
file |
diff |
annotate
|
| 2008-04-22 |
haftmann |
dropped theory PreList
|
file |
diff |
annotate
|
| 2008-04-22 |
haftmann |
added theory Sublist_Order
|
file |
diff |
annotate
|
| 2008-04-16 |
wenzelm |
removed unused TLA/Memory/MIParameters.thy;
|
file |
diff |
annotate
|
| 2008-04-08 |
krauss |
fixed makefiles
|
file |
diff |
annotate
|
| 2008-03-20 |
haftmann |
added theory Library/Enum.thy
|
file |
diff |
annotate
|
| 2008-03-14 |
nipkow |
Added lemmas
|
file |
diff |
annotate
|
| 2008-03-12 |
haftmann |
separated Random.thy from Quickcheck.thy
|
file |
diff |
annotate
|
| 2008-03-07 |
haftmann |
canonical order on option type
|
file |
diff |
annotate
|
| 2008-03-04 |
urbanc |
added new example
|
file |
diff |
annotate
|
| 2008-03-03 |
krauss |
new theory of red-black trees, an efficient implementation of finite maps.
|
file |
diff |
annotate
|
| 2008-02-27 |
haftmann |
added theories for imperative HOL
|
file |
diff |
annotate
|
| 2008-02-27 |
chaieb |
HOL/Dense_Linear_Order.thy moved to Library ; resulting dependencies updated
|
file |
diff |
annotate
|
| 2008-02-25 |
chaieb |
Added dependency of Library on Pocklington.thy
|
file |
diff |
annotate
|
| 2008-02-25 |
chaieb |
Included theories Library/Univ_Poly.thy and Complex/Fundamental_Theorem_Algebra.thy ; Theory Hyperreal/Poly.thy Removed
|
file |
diff |
annotate
|
| 2008-02-20 |
wenzelm |
removed ex/NBE.thy;
|
file |
diff |
annotate
|
| 2008-01-25 |
haftmann |
distinguished examples for Efficient_Nat.thy
|
file |
diff |
annotate
|
| 2008-01-15 |
haftmann |
joined theories IntDef, Numeral, IntArith to theory Int
|
file |
diff |
annotate
|
| 2008-01-02 |
haftmann |
improved evaluation mechanism
|
file |
diff |
annotate
|
| 2007-12-20 |
wenzelm |
moved Pure/General/random_word.ML to Tools/random_word.ML;
|
file |
diff |
annotate
|
| 2007-12-20 |
wenzelm |
updated HOL-Nominal-Examples deps;
|
file |
diff |
annotate
|
| 2007-12-11 |
haftmann |
joined EvenOdd theory with Parity
|
file |
diff |
annotate
|
| 2007-12-07 |
krauss |
Adding "ex/Induction_Scheme.thy" to tests
|
file |
diff |
annotate
|
| 2007-12-06 |
haftmann |
added new primrec package
|
file |
diff |
annotate
|
| 2007-12-05 |
haftmann |
dropped Classpackage.thy
|
file |
diff |
annotate
|
| 2007-11-13 |
berghofe |
Added new program extraction examples.
|
file |
diff |
annotate
|
| 2007-11-06 |
wenzelm |
activated HOL-SizeChange;
|
file |
diff |
annotate
|
| 2007-11-06 |
wenzelm |
removed dependencies on Size_Change_Termination from HOL-Library;
|
file |
diff |
annotate
|
| 2007-11-06 |
krauss |
moved stuff about size change termination to its own session
|
file |
diff |
annotate
|
| 2007-11-05 |
kleing |
add root.bib for Word document
|
file |
diff |
annotate
|
| 2007-10-24 |
wenzelm |
fixed HOL-Statespace for case-sensitive file-system;
|
file |
diff |
annotate
|
| 2007-10-24 |
schirmer |
added Statespace library
|
file |
diff |
annotate
|
| 2007-10-12 |
haftmann |
consolidated naming conventions for code generator theories
|
file |
diff |
annotate
|
| 2007-10-08 |
haftmann |
integrated FixedPoint into Inductive
|
file |
diff |
annotate
|
| 2007-10-08 |
urbanc |
changed VC-Compatible to VC_Compatible
|
file |
diff |
annotate
|
| 2007-10-08 |
urbanc |
added the two new examples from Nominal to the build process
|
file |
diff |
annotate
|
| 2007-10-04 |
wenzelm |
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
|
file |
diff |
annotate
|
| 2007-09-29 |
kleing |
Added target for proof term sessions (those that need -p 2)
|
file |
diff |
annotate
|
| 2007-09-25 |
haftmann |
datatype interpretators for size and datatype_realizer
|
file |
diff |
annotate
|
| 2007-09-18 |
wenzelm |
moved Tools/integer.ML to Pure/General/integer.ML;
|
file |
diff |
annotate
|
| 2007-09-18 |
haftmann |
introduced generic concepts for theory interpretators
|
file |
diff |
annotate
|
| 2007-09-18 |
haftmann |
separated code for inductive sequences from inductive_codegen.ML
|
file |
diff |
annotate
|
| 2007-09-18 |
nipkow |
sorting
|
file |
diff |
annotate
|
| 2007-09-16 |
wenzelm |
added Induct/Common_Patterns.thy;
|
file |
diff |
annotate
|
| 2007-09-06 |
berghofe |
- New theories Lambda/NormalForm and Lambda/Standardization
|
file |
diff |
annotate
|
| 2007-08-29 |
wenzelm |
added Hoare/hoare_tac.ML (code from Hoare/Hoare.thy, also required in Isar_examples/Hoare.thy);
|
file |
diff |
annotate
|
| 2007-08-29 |
wenzelm |
removed Hoare/hoare.ML, Hoare/hoareAbort.ML, ex/svc_oracle.ML (which can be mistaken as attached ML script on case-insensitive file-system);
|
file |
diff |
annotate
|
| 2007-08-28 |
huffman |
revert to Word library version from 2007/08/20
|
file |
diff |
annotate
|
| 2007-08-28 |
berghofe |
codegen.ML is now loaded in Pure again.
|
file |
diff |
annotate
|
| 2007-08-28 |
huffman |
HOL-Word-Examples
|
file |
diff |
annotate
|
| 2007-08-23 |
huffman |
Word/BinInduct.thy
|
file |
diff |
annotate
|
| 2007-08-22 |
huffman |
removed Word/Size.thy;
|
file |
diff |
annotate
|
| 2007-08-22 |
huffman |
Word/WordBoolList.thy
|
file |
diff |
annotate
|
| 2007-08-20 |
wenzelm |
use HOL-ex later;
|
file |
diff |
annotate
|
| 2007-08-20 |
huffman |
Word/document/root.tex
|
file |
diff |
annotate
|