berghofe [Fri, 21 Jun 1996 12:18:50 +0200] rev 1820
Classical tactics now use default claset.
oheimb [Fri, 21 Jun 1996 11:57:00 +0200] rev 1819
minor fix of index_vnames: name "O" is occupied (used in HOL/Relation.thy)
paulson [Thu, 20 Jun 1996 10:27:29 +0200] rev 1818
Restored Addsimps [Suc_le_lessD], as it cannot be added
to base HOL
paulson [Thu, 20 Jun 1996 10:26:13 +0200] rev 1817
Corrected comment
paulson [Tue, 18 Jun 1996 16:38:48 +0200] rev 1816
New rewrites for vacuous quantification
paulson [Tue, 18 Jun 1996 16:37:47 +0200] rev 1815
Addition of setOfList
paulson [Tue, 18 Jun 1996 16:36:04 +0200] rev 1814
Addition of Safe_step_tac
paulson [Tue, 18 Jun 1996 16:27:04 +0200] rev 1813
Translation infixes <->, etc., no longer available at top-level
paulson [Tue, 18 Jun 1996 16:20:30 +0200] rev 1812
Addition of setOfList
paulson [Tue, 18 Jun 1996 16:18:44 +0200] rev 1811
Removal of list_all
paulson [Tue, 18 Jun 1996 16:17:38 +0200] rev 1810
Translation infixes <->, etc., no longer available at top-level
paulson [Mon, 17 Jun 1996 16:51:47 +0200] rev 1809
Inserted comment about problem 43
paulson [Mon, 17 Jun 1996 16:51:11 +0200] rev 1808
Removed quantification over lists
paulson [Mon, 17 Jun 1996 16:50:38 +0200] rev 1807
Now exports Delrules
paulson [Mon, 17 Jun 1996 16:50:08 +0200] rev 1806
Converted to use constdefs instead of defs
paulson [Fri, 14 Jun 1996 12:37:21 +0200] rev 1805
Explicitly included add_mult_distrib & add_mult_distrib2
paulson [Fri, 14 Jun 1996 12:34:56 +0200] rev 1804
New example of greatest common divisor
paulson [Fri, 14 Jun 1996 12:32:08 +0200] rev 1803
Added Primes to list of theories in target ex
paulson [Fri, 14 Jun 1996 12:27:48 +0200] rev 1802
Now del_simp catches the right exception!
paulson [Fri, 14 Jun 1996 12:27:11 +0200] rev 1801
Added delete function for brls
paulson [Fri, 14 Jun 1996 12:26:06 +0200] rev 1800
Now implements delrules
paulson [Fri, 14 Jun 1996 12:25:19 +0200] rev 1799
Added new Primes theory
paulson [Fri, 14 Jun 1996 12:25:02 +0200] rev 1798
Explicitly included add_mult_distrib & add_mult_distrib2
paulson [Fri, 14 Jun 1996 12:23:31 +0200] rev 1797
Updated list of theories for target ex
paulson [Fri, 14 Jun 1996 12:22:59 +0200] rev 1796
Tidied spacing
paulson [Fri, 14 Jun 1996 12:22:42 +0200] rev 1795
New lemmas for gcd example
paulson [Fri, 14 Jun 1996 12:21:02 +0200] rev 1794
Obsolete relics concerned with recursion
paulson [Thu, 13 Jun 1996 16:22:37 +0200] rev 1793
New example of GCDs and divides relation
paulson [Thu, 13 Jun 1996 14:25:45 +0200] rev 1792
The "divides" relation, the greatest common divisor and Euclid's algorithm
paulson [Fri, 07 Jun 1996 10:56:37 +0200] rev 1791
Addition of converse_iff, domain_converse, range_converse as rewrites
paulson [Thu, 06 Jun 1996 16:20:27 +0200] rev 1790
Quotes now optional around inductive set
paulson [Thu, 06 Jun 1996 14:39:44 +0200] rev 1789
Quotes now optional around inductive set
paulson [Thu, 06 Jun 1996 13:13:18 +0200] rev 1788
Quotes now optional around inductive set
paulson [Tue, 04 Jun 1996 12:49:04 +0200] rev 1787
Tidied some proofs
berghofe [Mon, 03 Jun 1996 17:10:56 +0200] rev 1786
best_tac, deepen_tac and safe_tac now also use default claset.
paulson [Mon, 03 Jun 1996 11:44:44 +0200] rev 1785
Shortened some proofs
paulson [Mon, 03 Jun 1996 11:43:55 +0200] rev 1784
Added a new theorem, UN_Int_subset
paulson [Mon, 03 Jun 1996 11:41:26 +0200] rev 1783
Used 2 instead of Suc(Suc 0)
paulson [Mon, 03 Jun 1996 11:41:00 +0200] rev 1782
Shortened a proof
oheimb [Fri, 31 May 1996 20:25:59 +0200] rev 1781
adapted use of monofun_cfun_arg
oheimb [Fri, 31 May 1996 20:14:42 +0200] rev 1780
adapted proof of flat_codom
oheimb [Fri, 31 May 1996 19:55:19 +0200] rev 1779
introduced forgotten bind_thm calls
oheimb [Fri, 31 May 1996 19:47:23 +0200] rev 1778
adapted some proofs for new simplifier
oheimb [Fri, 31 May 1996 19:34:40 +0200] rev 1777
renamed le_0 to le_0_eq, to avoid confusion with le0,
supplied an experimental thm Suc_le_eq, but commented it out
oheimb [Fri, 31 May 1996 19:12:00 +0200] rev 1776
moved mem_simps and the corresponding update of !simpset from Fun.ML to Set.ML,
as there have been unnecessary proofs of anonymous thms, which could not be
removed (by name) from the !simpset where necessary. All these thms except
singleton_iff were already proved in Set.ML.
therefore in Set.ML: New version of singletonE, proof of new thm singleton_iff
nipkow [Thu, 30 May 1996 13:31:29 +0200] rev 1775
Smaller logo
nipkow [Thu, 30 May 1996 13:29:52 +0200] rev 1774
Regrouped logo
nipkow [Wed, 29 May 1996 13:53:39 +0200] rev 1773
Added logo
nipkow [Wed, 29 May 1996 13:47:43 +0200] rev 1772
An Isabelle logo
nipkow [Wed, 29 May 1996 13:34:17 +0200] rev 1771
Replaced setsolver by addsolver
nipkow [Wed, 29 May 1996 12:03:32 +0200] rev 1770
Added addsolver
paulson [Tue, 28 May 1996 11:19:16 +0200] rev 1769
Simplified proof of deduction theorem
paulson [Tue, 28 May 1996 11:16:38 +0200] rev 1768
Corrected a comment in #34
berghofe [Fri, 24 May 1996 12:27:04 +0200] rev 1767
Rules pred_0, pred_Suc etc. are now stored in theorem database.
nipkow [Fri, 24 May 1996 11:48:18 +0200] rev 1766
Modified proof of "(R^=)^* = R^*" to accommodate equalityI.
nipkow [Fri, 24 May 1996 11:46:40 +0200] rev 1765
Removed junk introduced by a cvs merge.
paulson [Fri, 24 May 1996 11:42:04 +0200] rev 1764
Augmented comment about conversion to clauses
berghofe [Thu, 23 May 1996 15:17:23 +0200] rev 1763
expanded TABs
berghofe [Thu, 23 May 1996 15:16:12 +0200] rev 1762
equalityI is now added to default claset
berghofe [Thu, 23 May 1996 15:15:20 +0200] rev 1761
Removed equalityI from some proofs (because it is now included
in the default claset)