| 1999-07-08 |
paulson |
new files IntDiv.{thy,ML}
|
file |
diff |
annotate
|
| 1999-07-06 |
wenzelm |
added Numeral.thy, Tools/numeral_syntax.ML;
|
file |
diff |
annotate
|
| 1999-07-01 |
wenzelm |
Isar_examples/KnasterTarski.thy;
|
file |
diff |
annotate
|
| 1999-06-11 |
paulson |
new UNITY files
|
file |
diff |
annotate
|
| 1999-06-04 |
wenzelm |
Calculation.thy: Setup transitivity rules for calculational proofs.
|
file |
diff |
annotate
|
| 1999-06-04 |
wenzelm |
added Isar_examples/Group.thy;
|
file |
diff |
annotate
|
| 1999-05-26 |
wenzelm |
ex/Points Isar'ized;
|
file |
diff |
annotate
|
| 1999-05-26 |
paulson |
new theories Follows and ListOrder
|
file |
diff |
annotate
|
| 1999-04-28 |
paulson |
eliminated theory UNITY/Traces
|
file |
diff |
annotate
|
| 1999-04-27 |
wenzelm |
added Isar_examples/NatSum.thy;
|
file |
diff |
annotate
|
| 1999-04-27 |
wenzelm |
added Isar_examples/Cantor.ML;
|
file |
diff |
annotate
|
| 1999-04-23 |
paulson |
Addition of Auth/KerberosIV; renaming of rules.new.sml to rules.sml
|
file |
diff |
annotate
|
| 1999-04-22 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 1999-04-22 |
mueller |
deleted some old examples in Modelcheck;
|
file |
diff |
annotate
|
| 1999-04-16 |
wenzelm |
added Isar_examples;
|
file |
diff |
annotate
|
| 1999-04-16 |
wenzelm |
added Tools/induct_method.ML;
|
file |
diff |
annotate
|
| 1999-04-14 |
wenzelm |
Tools/inductive_package.ML;
|
file |
diff |
annotate
|
| 1999-03-18 |
paulson |
added new theory Yahalom_Bad
|
file |
diff |
annotate
|
| 1999-03-03 |
paulson |
added UNITY/Extend
|
file |
diff |
annotate
|
| 1999-02-08 |
wenzelm |
updated TLA;
|
file |
diff |
annotate
|
| 1999-02-05 |
wenzelm |
Hyperreal made part of Real;
|
file |
diff |
annotate
|
| 1999-01-04 |
nipkow |
Version 1.0 of linear nat arithmetic.
|
file |
diff |
annotate
|
| 1998-11-27 |
nipkow |
At last: linear arithmetic for nat!
|
file |
diff |
annotate
|
| 1998-11-27 |
paulson |
added Real/Hyperreal
|
file |
diff |
annotate
|
| 1998-11-17 |
paulson |
new theory UNITY/PPROD
|
file |
diff |
annotate
|
| 1998-10-23 |
narasche |
ex/Points added
|
file |
diff |
annotate
|
| 1998-10-23 |
berghofe |
Directory Induct: Added new theory ABexp, removed obsolete
|
file |
diff |
annotate
|
| 1998-10-21 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 1998-10-20 |
wenzelm |
split_paired_all.ML;
|
file |
diff |
annotate
|
| 1998-10-13 |
paulson |
Addition of HOL/UNITY/Client
|
file |
diff |
annotate
|
| 1998-10-09 |
nipkow |
added Induct/Multiset*
|
file |
diff |
annotate
|
| 1998-10-07 |
paulson |
new files UNITY/Comp.{thy,ML}
|
file |
diff |
annotate
|
| 1998-10-06 |
nipkow |
Merges FoldSet into Finite
|
file |
diff |
annotate
|
| 1998-10-02 |
paulson |
new files Provers/Arith/abel_cancel.ML and Real/simproc.ML
|
file |
diff |
annotate
|
| 1998-09-25 |
paulson |
Renaming of Integ/Integ.* to Integ/Int.*
|
file |
diff |
annotate
|
| 1998-09-18 |
paulson |
new files in Integ
|
file |
diff |
annotate
|
| 1998-09-07 |
paulson |
New UNITY theory, the N-S protocol
|
file |
diff |
annotate
|
| 1998-09-01 |
paulson |
new theory Induct/FoldSet
|
file |
diff |
annotate
|
| 1998-08-24 |
wenzelm |
added Antiquote example;
|
file |
diff |
annotate
|
| 1998-08-21 |
paulson |
New UNITY files
|
file |
diff |
annotate
|
| 1998-08-17 |
nipkow |
Additions to Lex.
|
file |
diff |
annotate
|
| 1998-08-12 |
oheimb |
cleanup for Fun.thy:
|
file |
diff |
annotate
|
| 1998-08-06 |
nipkow |
New lemmas in List and Lambda in IsaMakefile
|
file |
diff |
annotate
|
| 1998-08-04 |
wenzelm |
added LocaleGroup, PiSets examples;
|
file |
diff |
annotate
|
| 1998-07-31 |
paulson |
Removed HOL/IMP/Com.ML because it contained only an "open" declaration
|
file |
diff |
annotate
|
| 1998-07-24 |
wenzelm |
added ex/MonoidGroups (record example);
|
file |
diff |
annotate
|
| 1998-07-24 |
berghofe |
Adapted to new datatype package.
|
file |
diff |
annotate
|
| 1998-07-03 |
wenzelm |
stepping stones: Recdef, Main;
|
file |
diff |
annotate
|
| 1998-07-02 |
wenzelm |
fixed Integ;
|
file |
diff |
annotate
|
| 1998-06-30 |
berghofe |
Adapted to new inductive definition package.
|
file |
diff |
annotate
|
| 1998-06-25 |
paulson |
Installation of target HOL-Real
|
file |
diff |
annotate
|
| 1998-06-11 |
nipkow |
removed rel.ML
|
file |
diff |
annotate
|
| 1998-05-11 |
nipkow |
Lex
|
file |
diff |
annotate
|
| 1998-05-05 |
paulson |
New syntax for function update; moved to main HOL directory
|
file |
diff |
annotate
|
| 1998-04-29 |
wenzelm |
removed typedef.ML, record.ML;
|
file |
diff |
annotate
|
| 1998-04-27 |
nipkow |
Added a few lemmas.
|
file |
diff |
annotate
|
| 1998-04-03 |
paulson |
New target HOL-UNITY
|
file |
diff |
annotate
|
| 1998-03-11 |
nipkow |
More Lex.
|
file |
diff |
annotate
|
| 1998-03-09 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| 1998-02-26 |
paulson |
New theory, Vimage
|
file |
diff |
annotate
|