Fri, 28 Jun 1996 11:10:32 +0200 |
paulson |
Restored warning comment
|
changeset |
files
|
Thu, 27 Jun 1996 15:24:17 +0200 |
oheimb |
re-added when_funs to library.ML
|
changeset |
files
|
Thu, 27 Jun 1996 15:19:50 +0200 |
oheimb |
patches for Holcfb.thy removed
|
changeset |
files
|
Thu, 27 Jun 1996 12:53:08 +0200 |
oheimb |
removed old version of LEAST operator
|
changeset |
files
|
Wed, 26 Jun 1996 17:50:10 +0200 |
oheimb |
repaired 8bit pragma
|
changeset |
files
|
Wed, 26 Jun 1996 17:45:32 +0200 |
oheimb |
adapted path to 8bit package
|
changeset |
files
|
Wed, 26 Jun 1996 17:38:34 +0200 |
oheimb |
function names in when_rews now meta-quantified
|
changeset |
files
|
Wed, 26 Jun 1996 17:37:34 +0200 |
oheimb |
when_funs removed
|
changeset |
files
|
Tue, 25 Jun 1996 18:01:37 +0200 |
oheimb |
*** empty log message ***
|
changeset |
files
|
Tue, 25 Jun 1996 17:44:43 +0200 |
oheimb |
Initial revision
|
changeset |
files
|
Tue, 25 Jun 1996 13:18:54 +0200 |
berghofe |
Changed argument order of nat_rec.
|
changeset |
files
|
Tue, 25 Jun 1996 13:11:29 +0200 |
berghofe |
Changed argument order of nat_rec.
|
changeset |
files
|
Fri, 21 Jun 1996 13:51:09 +0200 |
berghofe |
Replaced occurrence of fast_tac by Fast_tac .
|
changeset |
files
|
Fri, 21 Jun 1996 13:39:08 +0200 |
berghofe |
Replaced occurrence of set_cs by claset_of "Fun" .
|
changeset |
files
|
Fri, 21 Jun 1996 13:34:55 +0200 |
berghofe |
Added function Addss.
|
changeset |
files
|
Fri, 21 Jun 1996 12:18:50 +0200 |
berghofe |
Classical tactics now use default claset.
|
changeset |
files
|
Fri, 21 Jun 1996 11:57:00 +0200 |
oheimb |
minor fix of index_vnames: name "O" is occupied (used in HOL/Relation.thy)
|
changeset |
files
|
Thu, 20 Jun 1996 10:27:29 +0200 |
paulson |
Restored Addsimps [Suc_le_lessD], as it cannot be added
|
changeset |
files
|
Thu, 20 Jun 1996 10:26:13 +0200 |
paulson |
Corrected comment
|
changeset |
files
|
Tue, 18 Jun 1996 16:38:48 +0200 |
paulson |
New rewrites for vacuous quantification
|
changeset |
files
|
Tue, 18 Jun 1996 16:37:47 +0200 |
paulson |
Addition of setOfList
|
changeset |
files
|
Tue, 18 Jun 1996 16:36:04 +0200 |
paulson |
Addition of Safe_step_tac
|
changeset |
files
|
Tue, 18 Jun 1996 16:27:04 +0200 |
paulson |
Translation infixes <->, etc., no longer available at top-level
|
changeset |
files
|
Tue, 18 Jun 1996 16:20:30 +0200 |
paulson |
Addition of setOfList
|
changeset |
files
|
Tue, 18 Jun 1996 16:18:44 +0200 |
paulson |
Removal of list_all
|
changeset |
files
|
Tue, 18 Jun 1996 16:17:38 +0200 |
paulson |
Translation infixes <->, etc., no longer available at top-level
|
changeset |
files
|
Mon, 17 Jun 1996 16:51:47 +0200 |
paulson |
Inserted comment about problem 43
|
changeset |
files
|
Mon, 17 Jun 1996 16:51:11 +0200 |
paulson |
Removed quantification over lists
|
changeset |
files
|
Mon, 17 Jun 1996 16:50:38 +0200 |
paulson |
Now exports Delrules
|
changeset |
files
|
Mon, 17 Jun 1996 16:50:08 +0200 |
paulson |
Converted to use constdefs instead of defs
|
changeset |
files
|