| Thu, 27 Oct 2005 18:25:33 +0200 | paulson | sorted lemma lists | changeset | files |
| Thu, 27 Oct 2005 13:59:06 +0200 | wenzelm | * HOL: alternative iff syntax; | changeset | files |
| Thu, 27 Oct 2005 13:54:43 +0200 | wenzelm | consts: monomorphic; | changeset | files |
| Thu, 27 Oct 2005 13:54:42 +0200 | wenzelm | removed inappropriate monomorphic test; | changeset | files |
| Thu, 27 Oct 2005 13:54:40 +0200 | wenzelm | replaced Defs.monomorphic by Sign.monomorphic; | changeset | files |
| Thu, 27 Oct 2005 13:54:38 +0200 | wenzelm | alternative iff syntax for equality on booleans, with print_mode 'iff'; | changeset | files |
| Thu, 27 Oct 2005 08:14:05 +0200 | haftmann | added module Pure/General/rat.ML | changeset | files |
| Wed, 26 Oct 2005 16:31:53 +0200 | paulson | tidied away duplicate thm | changeset | files |
| Tue, 25 Oct 2005 18:38:21 +0200 | wenzelm | EVERY; | changeset | files |
| Tue, 25 Oct 2005 18:18:59 +0200 | wenzelm | traceIt: plain term; | changeset | files |
| Tue, 25 Oct 2005 18:18:58 +0200 | wenzelm | val legacy = ref false; | changeset | files |
| Tue, 25 Oct 2005 18:18:57 +0200 | wenzelm | prove_raw: cterms, explicit asms; | changeset | files |
| Tue, 25 Oct 2005 18:18:49 +0200 | wenzelm | avoid legacy goals; | changeset | files |
| Sat, 22 Oct 2005 01:22:10 +0200 | wenzelm | legacy = ref true for the time being -- avoid volumious warnings; | changeset | files |
| Fri, 21 Oct 2005 18:20:29 +0200 | wenzelm | tuned; | changeset | files |
| Fri, 21 Oct 2005 18:17:00 +0200 | wenzelm | avoid OldGoals shortcuts; | changeset | files |
| Fri, 21 Oct 2005 18:16:57 +0200 | wenzelm | * Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running. | changeset | files |
| Fri, 21 Oct 2005 18:15:00 +0200 | wenzelm | Internal goals. | changeset | files |
| Fri, 21 Oct 2005 18:14:59 +0200 | wenzelm | renamed triv_goal to goalI, rev_triv_goal to goalD; | changeset | files |
| Fri, 21 Oct 2005 18:14:58 +0200 | wenzelm | tuned header; | changeset | files |
| Fri, 21 Oct 2005 18:14:57 +0200 | wenzelm | Goal.norm_hhf_rule; | changeset | files |
| Fri, 21 Oct 2005 18:14:56 +0200 | wenzelm | export add_binds_i; | changeset | files |
| Fri, 21 Oct 2005 18:14:55 +0200 | wenzelm | load_file: setmp OldGoals.legacy true; | changeset | files |
| Fri, 21 Oct 2005 18:14:54 +0200 | wenzelm | improved check_result; | changeset | files |
| Fri, 21 Oct 2005 18:14:53 +0200 | wenzelm | Goal.prove_plain; | changeset | files |
| Fri, 21 Oct 2005 18:14:52 +0200 | wenzelm | do not export find_thms; | changeset | files |
| Fri, 21 Oct 2005 18:14:51 +0200 | wenzelm | use obsolete goals.ML here; | changeset | files |
| Fri, 21 Oct 2005 18:14:50 +0200 | wenzelm | Goal.conclude; | changeset | files |
| Fri, 21 Oct 2005 18:14:49 +0200 | wenzelm | moved SELECT_GOAL to goal.ML; | changeset | files |
| Fri, 21 Oct 2005 18:14:48 +0200 | wenzelm | moved norm_hhf_rule, prove etc. to goal.ML; | changeset | files |