| Wed, 18 Aug 1999 17:31:53 +0200 | wenzelm | tuned messages; | changeset | files |
| Wed, 18 Aug 1999 17:15:51 +0200 | wenzelm | tuned; | changeset | files |
| Wed, 18 Aug 1999 16:19:53 +0200 | berghofe | Renamed sum_case to basic_sum_case. | changeset | files |
| Wed, 18 Aug 1999 16:19:01 +0200 | berghofe | Eliminated some infixes. | changeset | files |
| Wed, 18 Aug 1999 16:12:20 +0200 | berghofe | Eliminated some infixes. | changeset | files |
| Wed, 18 Aug 1999 16:11:14 +0200 | berghofe | Renamed sum_case to basic_sum_case and removed translations for sum_case | changeset | files |
| Wed, 18 Aug 1999 16:05:27 +0200 | wenzelm | tuned; | changeset | files |
| Wed, 18 Aug 1999 16:04:00 +0200 | wenzelm | replaced 'ProofGeneral' by 'Proof General'; | changeset | files |
| Wed, 18 Aug 1999 15:40:45 +0200 | berghofe | Modified section about generation of theory browsing information. | changeset | files |
| Wed, 18 Aug 1999 12:23:10 +0200 | paulson | new version from Konrad with "lazy" (deferred) definitons | changeset | files |
| Wed, 18 Aug 1999 11:49:46 +0200 | paulson | tidied some proofs | changeset | files |
| Wed, 18 Aug 1999 10:54:44 +0200 | paulson | new primitive rule permute_prems to underlie defer_tac and rotate_prems | changeset | files |
| Wed, 18 Aug 1999 10:54:03 +0200 | paulson | freeze_thaw does nothing if no variables | changeset | files |
| Wed, 18 Aug 1999 10:27:57 +0200 | nipkow | Added take_all and drop_all to simpset. | changeset | files |
| Tue, 17 Aug 1999 22:24:15 +0200 | wenzelm | eliminated HOL_quantifiers (replaced by "HOL" print mode); | changeset | files |
| Tue, 17 Aug 1999 22:22:36 +0200 | wenzelm | may_load_file; | changeset | files |
| Tue, 17 Aug 1999 22:19:48 +0200 | wenzelm | ThyInfo.may_load_file; | changeset | files |
| Tue, 17 Aug 1999 22:19:25 +0200 | wenzelm | begin_update_theory; | changeset | files |
| Tue, 17 Aug 1999 22:16:21 +0200 | wenzelm | PASS(_MODE): works better without space (why?); | changeset | files |
| Tue, 17 Aug 1999 22:14:08 +0200 | wenzelm | removed HOL_quantifiers; | changeset | files |
| Tue, 17 Aug 1999 22:14:02 +0200 | wenzelm | HOL_quantifiers; | changeset | files |
| Tue, 17 Aug 1999 22:13:23 +0200 | wenzelm | replaced HOL_quantifiers flag by "HOL" print mode; | changeset | files |
| Tue, 17 Aug 1999 22:11:05 +0200 | wenzelm | turned SVC_Oracle into a new-style theory in order to get automatic | changeset | files |
| Tue, 17 Aug 1999 19:24:00 +0200 | berghofe | Better handling of path for remote theory browsing information. | changeset | files |
| Tue, 17 Aug 1999 17:52:04 +0200 | wenzelm | Goals.reset_goals; | changeset | files |
| Tue, 17 Aug 1999 17:51:35 +0200 | wenzelm | reset_goals; | changeset | files |
| Tue, 17 Aug 1999 17:34:43 +0200 | wenzelm | intro+; | changeset | files |
| Tue, 17 Aug 1999 17:34:18 +0200 | wenzelm | remove tmp files; | changeset | files |
| Tue, 17 Aug 1999 17:33:47 +0200 | wenzelm | tuned; | changeset | files |
| Tue, 17 Aug 1999 17:30:08 +0200 | wenzelm | renamed 'single' to 'some_rule'; | changeset | files |
| Tue, 17 Aug 1999 15:59:32 +0200 | wenzelm | renamed Cons to Consq in order to avoid clash with List.Cons; | changeset | files |
| Tue, 17 Aug 1999 14:01:39 +0200 | berghofe | Tuned some comments. | changeset | files |
| Tue, 17 Aug 1999 14:00:30 +0200 | berghofe | Path for remote theory browsing information is now stored in referece variable rpath. | changeset | files |
| Tue, 17 Aug 1999 11:51:12 +0200 | wenzelm | -m option; | changeset | files |
| Mon, 16 Aug 1999 22:08:23 +0200 | wenzelm | replaced "op #" by "Cons"; | changeset | files |
| Mon, 16 Aug 1999 22:07:12 +0200 | wenzelm | 'a list: Nil, Cons; | changeset | files |
| Mon, 16 Aug 1999 22:04:07 +0200 | wenzelm | tuned msg; | changeset | files |
| Mon, 16 Aug 1999 22:03:48 +0200 | wenzelm | disable_pr, enable_pr; | changeset | files |
| Mon, 16 Aug 1999 18:47:20 +0200 | paulson | deleted obsolete assignment | changeset | files |
| Mon, 16 Aug 1999 18:43:13 +0200 | paulson | restored a high precedence to unary minus | changeset | files |
| Mon, 16 Aug 1999 18:41:32 +0200 | paulson | inserted Id: lines | changeset | files |
| Mon, 16 Aug 1999 18:41:06 +0200 | paulson | new theory Real/Hyperreal/HyperDef and file fuf.ML | changeset | files |
| Mon, 16 Aug 1999 17:44:14 +0200 | oheimb | forgot to write back adaption of onlysimps | changeset | files |
| Mon, 16 Aug 1999 17:42:37 +0200 | wenzelm | tuned; | changeset | files |
| Mon, 16 Aug 1999 17:38:52 +0200 | wenzelm | tuned; | changeset | files |
| Mon, 16 Aug 1999 17:33:45 +0200 | oheimb | exchanged finish_tac and unsafe_finish_tac (the more important one) in simpset | changeset | files |
| Mon, 16 Aug 1999 17:24:28 +0200 | oheimb | re-added refl in safe_solver | changeset | files |
| Mon, 16 Aug 1999 16:44:47 +0200 | wenzelm | removed warn_theory_style; | changeset | files |
| Mon, 16 Aug 1999 16:44:24 +0200 | wenzelm | fixed thy_only; | changeset | files |
| Mon, 16 Aug 1999 15:15:14 +0200 | wenzelm | tuned prompts; | changeset | files |
| Mon, 16 Aug 1999 14:57:41 +0200 | wenzelm | isamode; | changeset | files |
| Mon, 16 Aug 1999 14:22:45 +0200 | wenzelm | user infaces: tuned, added ProofGeneral; | changeset | files |
| Mon, 16 Aug 1999 14:22:20 +0200 | wenzelm | bib; | changeset | files |
| Mon, 16 Aug 1999 11:53:18 +0200 | wenzelm | -m option; | changeset | files |
| Thu, 12 Aug 1999 15:35:03 +0200 | berghofe | Tuned. | changeset | files |
| Wed, 11 Aug 1999 13:14:31 +0200 | nipkow | Removed | changeset | files |
| Wed, 11 Aug 1999 13:13:58 +0200 | nipkow | * set HOL_quantifiers by default, i.e. quantifiers are printed as | changeset | files |
| Mon, 09 Aug 1999 22:25:27 +0200 | wenzelm | added asym rule; | changeset | files |
| Mon, 09 Aug 1999 22:23:07 +0200 | wenzelm | tuned print_state; | changeset | files |
| Mon, 09 Aug 1999 22:22:49 +0200 | wenzelm | tuned strings_of_context; | changeset | files |