| 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
|
| Tue, 06 Sep 2005 23:14:10 +0200 |
huffman |
add Hyperreal dependencies
|
file |
diff |
annotate
|
| Tue, 06 Sep 2005 18:49:25 +0200 |
wenzelm |
removed some ML files in Modelcheck/;
|
file |
diff |
annotate
|
| Fri, 02 Sep 2005 15:24:58 +0200 |
paulson |
deleted obsolete VampireCommunication.ML
|
file |
diff |
annotate
|
| Wed, 31 Aug 2005 15:46:35 +0200 |
wenzelm |
added Complex/ex/BigO_Complex.thy;
|
file |
diff |
annotate
|
| Fri, 05 Aug 2005 19:56:58 +0200 |
berghofe |
Added Extraction/Pigeonhole.
|
file |
diff |
annotate
|
| Wed, 03 Aug 2005 14:48:30 +0200 |
avigad |
added Hyperreal/Ln, replaced Lfp and Gfp by FixedPoint
|
file |
diff |
annotate
|
| Mon, 25 Jul 2005 18:54:49 +0200 |
avigad |
Added two new theories to HOL/Library: SetsAndFunctions.thy and BigO.thy
|
file |
diff |
annotate
|
| Tue, 19 Jul 2005 16:16:53 +0200 |
obua |
proving bounds for real linear programs
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 09:53:50 +0200 |
obua |
- added cplex package to HOL/Matrix
|
file |
diff |
annotate
|
| Tue, 12 Jul 2005 21:49:38 +0200 |
obua |
- use TableFun instead of homebrew binary tree in am_interpreter.ML
|
file |
diff |
annotate
|
| Thu, 07 Jul 2005 12:39:17 +0200 |
nipkow |
linear arithmetic now takes "&" in assumptions apart.
|
file |
diff |
annotate
|
| Tue, 21 Jun 2005 09:31:57 +0200 |
wenzelm |
fixed HOL-Complex-Matrix target;
|
file |
diff |
annotate
|
| Mon, 20 Jun 2005 22:13:57 +0200 |
wenzelm |
HOL-Matrix: plain session;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2005 23:33:28 +0200 |
wenzelm |
added Isar_examples/Drinker.thy;
|
file |
diff |
annotate
|
| Thu, 02 Jun 2005 18:29:47 +0200 |
wenzelm |
renamed HOL_PROOF_OBJECTS to HOL_USEDIR_OPTIONS;
|
file |
diff |
annotate
|
| Thu, 26 May 2005 16:50:20 +0200 |
paulson |
goodby to modUnix
|
file |
diff |
annotate
|
| Sun, 22 May 2005 16:51:07 +0200 |
wenzelm |
Simplifier already setup in Pure;
|
file |
diff |
annotate
|
| Thu, 28 Apr 2005 17:08:08 +0200 |
bauerg |
*** empty log message ***
|
file |
diff |
annotate
|
| Wed, 27 Apr 2005 06:03:35 +0200 |
kleing |
reverted last change (dependencies in HOL)
|
file |
diff |
annotate
|
| Wed, 20 Apr 2005 16:03:17 +0200 |
quigley |
Removed remaining references to Main.thy in reconstruction code.
|
file |
diff |
annotate
|
| Tue, 19 Apr 2005 18:08:44 +0200 |
paulson |
more tidying of libraries in Reconstruction
|
file |
diff |
annotate
|
| Tue, 19 Apr 2005 13:34:50 +0200 |
paulson |
restored the target HOL-Complex-Import
|
file |
diff |
annotate
|
| Thu, 14 Apr 2005 17:57:04 +0200 |
nipkow |
Removed dir Orderings in Library
|
file |
diff |
annotate
|
| Mon, 11 Apr 2005 16:25:31 +0200 |
paulson |
removal of Main and other tidying up
|
file |
diff |
annotate
|
| Fri, 08 Apr 2005 18:43:39 +0200 |
paulson |
Reconstruction code, now packaged to avoid name clashes
|
file |
diff |
annotate
|
| Thu, 07 Apr 2005 17:45:51 +0200 |
quigley |
Reconstruction.thy and IsaMakefile updated
|
file |
diff |
annotate
|
| Mon, 04 Apr 2005 18:43:18 +0200 |
quigley |
Updated to add watcher code.
|
file |
diff |
annotate
|
| Fri, 01 Apr 2005 18:59:17 +0200 |
skalberg |
Updated import configuration.
|
file |
diff |
annotate
|
| Tue, 29 Mar 2005 12:30:48 +0200 |
paulson |
converted HOL-Subst to tactic scripts
|
file |
diff |
annotate
|
| Thu, 24 Mar 2005 16:34:15 +0100 |
ballarin |
Transitivity reasoner ignores types amenable to linear arithmetic.
|
file |
diff |
annotate
|
| Thu, 24 Mar 2005 10:59:21 +0100 |
paulson |
COMMENT IN WRONG PLACE
|
file |
diff |
annotate
|
| Wed, 23 Mar 2005 12:08:52 +0100 |
paulson |
temporary removal of Import
|
file |
diff |
annotate
|
| Mon, 07 Mar 2005 18:19:55 +0100 |
obua |
Cleaning up HOL/Matrix
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Wed, 09 Feb 2005 18:51:02 +0100 |
nipkow |
added lattice_locales
|
file |
diff |
annotate
|
| Tue, 01 Feb 2005 18:01:57 +0100 |
paulson |
the new subst tactic, by Lucas Dixon
|
file |
diff |
annotate
|
| Fri, 17 Dec 2004 10:15:46 +0100 |
paulson |
removed two looping simplifications in SetInterval.thy; deleted the .ML file
|
file |
diff |
annotate
|
| Wed, 15 Dec 2004 10:19:01 +0100 |
paulson |
removal of HOL_Lemmas
|
file |
diff |
annotate
|
| Tue, 14 Dec 2004 14:53:02 +0100 |
paulson |
converted Relation_Power to new-style theory
|
file |
diff |
annotate
|
| Mon, 13 Dec 2004 15:06:59 +0100 |
paulson |
removal of NatArith.ML and Product_Type.ML
|
file |
diff |
annotate
|
| Thu, 09 Dec 2004 16:45:46 +0100 |
paulson |
converted Sum_Type to new-style theory: Inl, Inr are NO LONGER global
|
file |
diff |
annotate
|
| Thu, 09 Dec 2004 12:03:06 +0100 |
paulson |
converted Datatype_Universe to new-style theory
|
file |
diff |
annotate
|
| Wed, 08 Dec 2004 10:28:05 +0100 |
paulson |
converted Lfp to new-style theory
|
file |
diff |
annotate
|