| Fri, 23 Mar 2007 09:40:47 +0100 |
haftmann |
removed outdated example
|
file |
diff |
annotate
|
| Tue, 20 Mar 2007 15:52:39 +0100 |
haftmann |
dropped OrderedGroup.ML
|
file |
diff |
annotate
|
| Fri, 16 Mar 2007 21:33:31 +0100 |
haftmann |
dropped LOrder.thy
|
file |
diff |
annotate
|
| Fri, 16 Mar 2007 17:17:36 +0100 |
urbanc |
adjusted for the example file SOS.thy
|
file |
diff |
annotate
|
| Wed, 28 Feb 2007 16:35:00 +0100 |
krauss |
more cleanup
|
file |
diff |
annotate
|
| Mon, 26 Feb 2007 21:34:16 +0100 |
krauss |
Added formalization of size-change principle (experimental).
|
file |
diff |
annotate
|
| Fri, 16 Feb 2007 09:04:23 +0100 |
krauss |
updated Makefile
|
file |
diff |
annotate
|
| Tue, 13 Feb 2007 18:19:25 +0100 |
berghofe |
Added new file Nominal/nominal_inductive.ML
|
file |
diff |
annotate
|
| Wed, 07 Feb 2007 17:26:04 +0100 |
berghofe |
Added Predicate theory.
|
file |
diff |
annotate
|
| Tue, 06 Feb 2007 00:53:15 +0100 |
urbanc |
corrected typo introduced by me
|
file |
diff |
annotate
|
| Tue, 06 Feb 2007 00:41:54 +0100 |
urbanc |
moved the infrastructure from the nominal_tags file to nominal_thmdecls
|
file |
diff |
annotate
|
| Mon, 22 Jan 2007 18:17:04 +0100 |
krauss |
Included ex/Fundefs.thy in HOL-ex session
|
file |
diff |
annotate
|
| Mon, 22 Jan 2007 17:29:43 +0100 |
krauss |
* Preliminary implementation of tail recursion
|
file |
diff |
annotate
|
| Sat, 20 Jan 2007 14:27:45 +0100 |
wenzelm |
added HOL/ex/Binary.thy;
|
file |
diff |
annotate
|
| Fri, 19 Jan 2007 22:08:07 +0100 |
wenzelm |
HOL-Lambda: usedir -m no_brackets;
|
file |
diff |
annotate
|
| Tue, 16 Jan 2007 14:11:25 +0100 |
urbanc |
fixed typo introduced by me
|
file |
diff |
annotate
|
| Tue, 16 Jan 2007 13:59:08 +0100 |
urbanc |
formalisation of Crary's chapter on logical relations
|
file |
diff |
annotate
|
| Tue, 16 Jan 2007 08:06:55 +0100 |
haftmann |
refined and added example for ExecutableRat
|
file |
diff |
annotate
|
| Wed, 03 Jan 2007 10:59:06 +0100 |
paulson |
first version of structured proof reconstruction
|
file |
diff |
annotate
|
| Wed, 27 Dec 2006 19:09:56 +0100 |
haftmann |
added code generator test theory
|
file |
diff |
annotate
|
| Sat, 16 Dec 2006 20:27:56 +0100 |
huffman |
removed Hyperreal/HyperArith.thy and Hyperreal/HyperPow.thy
|
file |
diff |
annotate
|
| Thu, 14 Dec 2006 22:19:39 +0100 |
huffman |
remove Hyperreal/fuf.ML
|
file |
diff |
annotate
|
| Tue, 12 Dec 2006 00:03:42 +0100 |
huffman |
Hyperreal/FrechetDeriv.thy
|
file |
diff |
annotate
|
| Sun, 10 Dec 2006 19:37:25 +0100 |
wenzelm |
added Tools/string_syntax.ML;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2006 01:12:36 +0100 |
wenzelm |
removed legacy ML bindings;
|
file |
diff |
annotate
|
| Mon, 04 Dec 2006 00:05:47 +0100 |
wenzelm |
converted legacy ML script;
|
file |
diff |
annotate
|
| Sat, 02 Dec 2006 02:52:02 +0100 |
wenzelm |
TLA: converted legacy ML scripts;
|
file |
diff |
annotate
|
| Mon, 27 Nov 2006 12:11:20 +0100 |
berghofe |
Added nominal_primrec.ML
|
file |
diff |
annotate
|
| Mon, 20 Nov 2006 21:23:12 +0100 |
wenzelm |
HOL-Prolog: converted legacy ML scripts;
|
file |
diff |
annotate
|
| Sun, 19 Nov 2006 23:48:55 +0100 |
wenzelm |
HOL-Algebra: converted legacy ML scripts;
|
file |
diff |
annotate
|
| Mon, 13 Nov 2006 11:41:40 +0100 |
krauss |
added lexicographic_order.ML to makefile
|
file |
diff |
annotate
|
| Wed, 08 Nov 2006 23:11:13 +0100 |
wenzelm |
moved theories Parity, GCD, Binomial to Library;
|
file |
diff |
annotate
|
| Wed, 08 Nov 2006 21:45:15 +0100 |
wenzelm |
incorporated former theories Reconstruction and ResAtpMethods into ATP_Linkup;
|
file |
diff |
annotate
|
| Wed, 08 Nov 2006 19:48:34 +0100 |
haftmann |
renamed Lattice_Locales to Lattices
|
file |
diff |
annotate
|
| Wed, 08 Nov 2006 13:48:33 +0100 |
wenzelm |
removed NatArith.thy, Main.ML;
|
file |
diff |
annotate
|
| Mon, 06 Nov 2006 16:28:33 +0100 |
haftmann |
added state monad to HOL library
|
file |
diff |
annotate
|
| Sat, 04 Nov 2006 00:11:11 +0100 |
huffman |
new Deriv.thy contains stuff from Lim.thy
|
file |
diff |
annotate
|
| Fri, 03 Nov 2006 14:22:37 +0100 |
haftmann |
simplified reasoning tools setup
|
file |
diff |
annotate
|
| Wed, 01 Nov 2006 19:03:30 +0100 |
urbanc |
changed to not compile Iteration and Recursion, but Lam_Funs instead
|
file |
diff |
annotate
|
| Thu, 26 Oct 2006 10:48:35 +0200 |
paulson |
Conversion to clause form now tolerates Boolean variables without looping.
|
file |
diff |
annotate
|
| Mon, 23 Oct 2006 00:47:25 +0200 |
berghofe |
Added Compile and Height examples to Nominal directory.
|
file |
diff |
annotate
|
| Fri, 20 Oct 2006 18:22:24 +0200 |
haftmann |
removed antisym_setup.ML
|
file |
diff |
annotate
|
| Mon, 16 Oct 2006 14:07:31 +0200 |
haftmann |
moved HOL code generator setup to Code_Generator
|
file |
diff |
annotate
|
| Fri, 13 Oct 2006 18:12:58 +0200 |
berghofe |
Added new package for inductive definitions, moved old package
|
file |
diff |
annotate
|
| Fri, 06 Oct 2006 03:49:36 +0200 |
kleing |
examples for hex and bin numerals
|
file |
diff |
annotate
|
| Sun, 01 Oct 2006 22:19:23 +0200 |
wenzelm |
removed obsolete Datatype_Universe.thy (cf. Datatype.thy);
|
file |
diff |
annotate
|
| Sun, 01 Oct 2006 18:29:25 +0200 |
wenzelm |
moved Infinite_Set.thy to Library;
|
file |
diff |
annotate
|
| Fri, 29 Sep 2006 22:47:51 +0200 |
wenzelm |
moved Matrix/cplex/MatrixLP.ML to Matrix/cplex/matrixlp.ML;
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 23:42:32 +0200 |
wenzelm |
removed obsolete Real/document/root.tex;
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 16:01:48 +0200 |
paulson |
clearout of obsolete code
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 18:18:11 +0200 |
wenzelm |
moved Import/susp.ML to Pure/General;
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 15:22:21 +0200 |
haftmann |
added OperationalEquality.thy
|
file |
diff |
annotate
|
| Tue, 19 Sep 2006 05:54:17 +0200 |
huffman |
add Real/RealVector.thy
|
file |
diff |
annotate
|
| Thu, 14 Sep 2006 15:25:23 +0200 |
krauss |
updated makefile
|
file |
diff |
annotate
|
| Wed, 30 Aug 2006 08:34:45 +0200 |
haftmann |
added yet another code generator example
|
file |
diff |
annotate
|
| Tue, 29 Aug 2006 14:31:12 +0200 |
haftmann |
added typecopy_package and some examples
|
file |
diff |
annotate
|
| Mon, 21 Aug 2006 11:02:39 +0200 |
haftmann |
added some codegen examples/applications
|
file |
diff |
annotate
|
| Mon, 14 Aug 2006 13:46:08 +0200 |
haftmann |
added new files
|
file |
diff |
annotate
|
| Tue, 08 Aug 2006 08:19:06 +0200 |
haftmann |
added Tools/typedef_codegen.ML
|
file |
diff |
annotate
|
| Thu, 03 Aug 2006 15:03:49 +0200 |
wenzelm |
added HOL/ex/Reflection;
|
file |
diff |
annotate
|
| Thu, 03 Aug 2006 14:57:26 +0200 |
ballarin |
Restructured algebra library, added ideals and quotient rings.
|
file |
diff |
annotate
|
| Tue, 04 Jul 2006 19:49:47 +0200 |
wenzelm |
added ex/Guess.thy;
|
file |
diff |
annotate
|
| Fri, 23 Jun 2006 09:55:01 +0200 |
paulson |
Introduction of Ramsey's theorem
|
file |
diff |
annotate
|
| Sun, 11 Jun 2006 00:42:22 +0200 |
dixon |
updated IsaMakefiles for new location of IsaPlanner.
|
file |
diff |
annotate
|
| Wed, 07 Jun 2006 01:51:22 +0200 |
wenzelm |
removed obsolete ML files;
|
file |
diff |
annotate
|
| Wed, 07 Jun 2006 01:06:53 +0200 |
wenzelm |
removed obsolete ML files;
|
file |
diff |
annotate
|
| Wed, 07 Jun 2006 00:57:14 +0200 |
wenzelm |
removed obsolete ML files;
|
file |
diff |
annotate
|
| Sun, 04 Jun 2006 10:50:41 +0200 |
mengj |
Functions of Tools/ATP/res_clasimpset.ML are now in Tools/res_atp.ML. res_clasimpset.ML is not used anymore.
|
file |
diff |
annotate
|
| Tue, 16 May 2006 13:01:22 +0200 |
wenzelm |
added Ferrante and Rackoff Algorithm -- by Amine Chaieb;
|
file |
diff |
annotate
|
| Fri, 05 May 2006 17:17:21 +0200 |
krauss |
First usable version of the new function definition package (HOL/function_packake/...).
|
file |
diff |
annotate
|
| Fri, 28 Apr 2006 17:56:20 +0200 |
berghofe |
Added Class, Fsub, and Lambda_mu examples for nominal datatypes.
|
file |
diff |
annotate
|
| Fri, 28 Apr 2006 15:59:31 +0200 |
berghofe |
Added new targets for nominal datatype package.
|
file |
diff |
annotate
|
| Mon, 10 Apr 2006 16:00:34 +0200 |
obua |
Moved stuff from Ring_and_Field to Matrix
|
file |
diff |
annotate
|
| Mon, 10 Apr 2006 11:35:02 +0200 |
nipkow |
Hoare(Parallel) dependencies on document/*
|
file |
diff |
annotate
|
| Fri, 10 Mar 2006 16:05:34 +0100 |
schirmer |
Added Library/AssocList.thy
|
file |
diff |
annotate
|
| Tue, 07 Mar 2006 16:03:31 +0100 |
obua |
Added HOL-ZF to Isabelle.
|
file |
diff |
annotate
|
| Tue, 07 Mar 2006 03:48:02 +0100 |
mengj |
Merged res_atp_setup.ML into res_atp.ML.
|
file |
diff |
annotate
|
| Wed, 01 Mar 2006 06:06:16 +0100 |
mengj |
Added file Tools/res_atpset.ML.
|
file |
diff |
annotate
|
| Fri, 17 Feb 2006 17:00:33 +0100 |
wenzelm |
removed Import/lazy_scan.ML;
|
file |
diff |
annotate
|
| Thu, 16 Feb 2006 21:11:58 +0100 |
wenzelm |
added ex/Abstract_NAT.thy;
|
file |
diff |
annotate
|
| Tue, 14 Feb 2006 17:07:48 +0100 |
haftmann |
added theory of executable rational numbers
|
file |
diff |
annotate
|
| Wed, 01 Feb 2006 15:22:02 +0100 |
paulson |
new and updated protocol proofs by Giamp Bella
|
file |
diff |
annotate
|
| Fri, 27 Jan 2006 05:45:25 +0100 |
mengj |
Added in new file Tools/ATP/reduce_axiomsN.ML
|
file |
diff |
annotate
|
| Fri, 06 Jan 2006 18:18:15 +0100 |
wenzelm |
removed obsolete eqrule_HOL_data.ML;
|
file |
diff |
annotate
|
| Sat, 31 Dec 2005 21:49:36 +0100 |
wenzelm |
removed obsolete Provers/make_elim.ML;
|
file |
diff |
annotate
|
| Thu, 22 Dec 2005 00:29:15 +0100 |
wenzelm |
added Provers/project_rule.ML
|
file |
diff |
annotate
|
| Wed, 21 Dec 2005 12:06:08 +0100 |
paulson |
new hash table module in HOL/Too/s
|
file |
diff |
annotate
|
| Fri, 16 Dec 2005 12:15:54 +0100 |
paulson |
hashing to eliminate the output of duplicate clauses
|
file |
diff |
annotate
|
| Wed, 14 Dec 2005 22:05:22 +0100 |
webertj |
ex/Sudoku.thy
|
file |
diff |
annotate
|
| Tue, 13 Dec 2005 19:32:04 +0100 |
wenzelm |
added HOL/Library/Coinductive_List.thy;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2005 02:30:53 +0200 |
mengj |
Added Tools/res_hol_clause.ML
|
file |
diff |
annotate
|
| Fri, 21 Oct 2005 02:57:22 +0200 |
mengj |
Merged theory ResAtpOracle.thy into ResAtpMethods.thy
|
file |
diff |
annotate
|
| Wed, 19 Oct 2005 21:52:31 +0200 |
wenzelm |
removed obsolete HOL/thy_syntax.ML;
|
file |
diff |
annotate
|
| Wed, 19 Oct 2005 06:33:24 +0200 |
mengj |
Added files in order to use external ATPs as oracles and invoke these ATPs by calling Isabelle methods (currently "vampire" and "eprover").
|
file |
diff |
annotate
|
| Fri, 14 Oct 2005 11:36:14 +0200 |
paulson |
deletion of Tools/res_types_sorts; removal of absolute numbering of clauses
|
file |
diff |
annotate
|
| Mon, 10 Oct 2005 15:35:29 +0200 |
paulson |
small tidy-up of utility functions
|
file |
diff |
annotate
|
| Sat, 08 Oct 2005 22:39:38 +0200 |
wenzelm |
added Import/susp.ML, Import/lazy_seq.ML, Import/lasy_scan.ML;
|
file |
diff |
annotate
|
| Fri, 07 Oct 2005 22:59:21 +0200 |
wenzelm |
removed obsolete ex/Tuple.thy;
|
file |
diff |
annotate
|
| Thu, 29 Sep 2005 00:59:03 +0200 |
wenzelm |
HOL4 image is back;
|
file |
diff |
annotate
|
| Mon, 26 Sep 2005 02:27:59 +0200 |
obua |
added entry for running HOLLight
|
file |
diff |
annotate
|
| Sun, 25 Sep 2005 20:17:13 +0200 |
berghofe |
Added ExecutableSet and Taylor.
|
file |
diff |
annotate
|
| Fri, 23 Sep 2005 22:58:50 +0200 |
webertj |
new sat tactic imports resolution proofs from zChaff
|
file |
diff |
annotate
|
| Fri, 23 Sep 2005 22:21:50 +0200 |
wenzelm |
tuned order of targets;
|
file |
diff |
annotate
|
| Wed, 21 Sep 2005 11:50:20 +0200 |
wenzelm |
HOL-Complex-Matrix: fixed deps;
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 14:17:31 +0200 |
wenzelm |
HOL-ex: Library/Commutative_Ring.thy;
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 14:13:20 +0200 |
wenzelm |
moved Tools/comm_ring.ML to Library;
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 13:58:58 +0200 |
wenzelm |
removed Commutative_Ring.thy, added HOL/ex/Chinese.thy;
|
file |
diff |
annotate
|
| Mon, 19 Sep 2005 19:49:09 +0200 |
obua |
Removed superfluous HOL/Matrix/cplex/ROOT.ML.
|
file |
diff |
annotate
|
| Mon, 19 Sep 2005 18:30:22 +0200 |
paulson |
further simplification of the Isabelle-ATP linkup
|
file |
diff |
annotate
|
| Mon, 19 Sep 2005 15:12:13 +0200 |
paulson |
simplification of the Isabelle-ATP code; hooks for batch generation of problems
|
file |
diff |
annotate
|
| Sat, 17 Sep 2005 18:11:20 +0200 |
wenzelm |
generate: added HOL-Complex-Generate-HOLLight;
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 23:53:33 +0200 |
huffman |
merge Hyperreal/Transfer.thy and Hyperreal/StarType.thy into Hyperreal/StarDef.thy
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 17:16:54 +0200 |
wenzelm |
added HOL/ex/Hebrew.thy;
|
file |
diff |
annotate
|
| Wed, 14 Sep 2005 23:14:57 +0200 |
wenzelm |
renamed Guard/NS_Public, Guard/OtwayRees, Guard/Yahalom.thy to avoid clash with plain Auth versions;
|
file |
diff |
annotate
|
| Wed, 14 Sep 2005 22:04:35 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 14 Sep 2005 17:25:52 +0200 |
chaieb |
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
|
file |
diff |
annotate
|
| Mon, 12 Sep 2005 23:07:58 +0200 |
huffman |
add file Hyperreal/transfer.ML
|
file |
diff |
annotate
|
| Mon, 12 Sep 2005 16:20:18 +0200 |
obua |
1) Added target HOL-Complex-Generate-HOLLight
|
file |
diff |
annotate
|
| Wed, 07 Sep 2005 20:22:15 +0200 |
wenzelm |
removed TLA/Inc/Pcount.thy;
|
file |
diff |
annotate
|
| Wed, 07 Sep 2005 09:53:50 +0200 |
paulson |
consolidation of watcher.ML and watcher.sig
|
file |
diff |
annotate
|