wenzelm [Thu, 27 Oct 2005 13:54:42 +0200] rev 17994
removed inappropriate monomorphic test;
wenzelm [Thu, 27 Oct 2005 13:54:40 +0200] rev 17993
replaced Defs.monomorphic by Sign.monomorphic;
wenzelm [Thu, 27 Oct 2005 13:54:38 +0200] rev 17992
alternative iff syntax for equality on booleans, with print_mode 'iff';
haftmann [Thu, 27 Oct 2005 08:14:05 +0200] rev 17991
added module Pure/General/rat.ML
paulson [Wed, 26 Oct 2005 16:31:53 +0200] rev 17990
tidied away duplicate thm
wenzelm [Tue, 25 Oct 2005 18:38:21 +0200] rev 17989
EVERY;
wenzelm [Tue, 25 Oct 2005 18:18:59 +0200] rev 17988
traceIt: plain term;
wenzelm [Tue, 25 Oct 2005 18:18:58 +0200] rev 17987
val legacy = ref false;
wenzelm [Tue, 25 Oct 2005 18:18:57 +0200] rev 17986
prove_raw: cterms, explicit asms;
prove: Pattern.matches beta_norm;
wenzelm [Tue, 25 Oct 2005 18:18:49 +0200] rev 17985
avoid legacy goals;
wenzelm [Sat, 22 Oct 2005 01:22:10 +0200] rev 17984
legacy = ref true for the time being -- avoid volumious warnings;
wenzelm [Fri, 21 Oct 2005 18:20:29 +0200] rev 17983
tuned;
wenzelm [Fri, 21 Oct 2005 18:17:00 +0200] rev 17982
avoid OldGoals shortcuts;
wenzelm [Fri, 21 Oct 2005 18:16:57 +0200] rev 17981
* Legacy goal package: reduced interface to the bare minimum required to keep existing proof scripts running.
* Internal goals: structure Goal.
wenzelm [Fri, 21 Oct 2005 18:15:00 +0200] rev 17980
Internal goals.
wenzelm [Fri, 21 Oct 2005 18:14:59 +0200] rev 17979
renamed triv_goal to goalI, rev_triv_goal to goalD;
wenzelm [Fri, 21 Oct 2005 18:14:58 +0200] rev 17978
tuned header;
wenzelm [Fri, 21 Oct 2005 18:14:57 +0200] rev 17977
Goal.norm_hhf_rule;
wenzelm [Fri, 21 Oct 2005 18:14:56 +0200] rev 17976
export add_binds_i;
invoke_case: AutoBind.no_facts;
Goal.init, Goal.conclude;
wenzelm [Fri, 21 Oct 2005 18:14:55 +0200] rev 17975
load_file: setmp OldGoals.legacy true;
wenzelm [Fri, 21 Oct 2005 18:14:54 +0200] rev 17974
improved check_result;
Goal.init, Goal.conclude;
wenzelm [Fri, 21 Oct 2005 18:14:53 +0200] rev 17973
Goal.prove_plain;
wenzelm [Fri, 21 Oct 2005 18:14:52 +0200] rev 17972
do not export find_thms;
wenzelm [Fri, 21 Oct 2005 18:14:51 +0200] rev 17971
use obsolete goals.ML here;
wenzelm [Fri, 21 Oct 2005 18:14:50 +0200] rev 17970
Goal.conclude;
wenzelm [Fri, 21 Oct 2005 18:14:49 +0200] rev 17969
moved SELECT_GOAL to goal.ML;
wenzelm [Fri, 21 Oct 2005 18:14:48 +0200] rev 17968
moved norm_hhf_rule, prove etc. to goal.ML;
moved asm_rewrite_goal_tac to simplifier.ML;
wenzelm [Fri, 21 Oct 2005 18:14:47 +0200] rev 17967
added simplification tactics and rules (from meta_simplifier.ML);
wenzelm [Fri, 21 Oct 2005 18:14:46 +0200] rev 17966
moved various simplification tactics and rules to simplifier.ML;
wenzelm [Fri, 21 Oct 2005 18:14:45 +0200] rev 17965
warn_obsolete for goal commands -- danger of disrupting a local proof context;
Goal.init, Goal.conclude, Goal.norm_hhf_rule;
shortcuts no longer pervasive (cf. structure OldGoals);