mengj [Fri, 28 Oct 2005 02:23:49 +0200] rev 17998
A new file that defines datatypes representing FOL clauses that are derived from HOL formulae. This file also has functions that convert lambda terms to combinator expressions, and functions that convert clauses to TPTP format.
paulson [Thu, 27 Oct 2005 18:25:33 +0200] rev 17997
sorted lemma lists
wenzelm [Thu, 27 Oct 2005 13:59:06 +0200] rev 17996
* HOL: alternative iff syntax;
wenzelm [Thu, 27 Oct 2005 13:54:43 +0200] rev 17995
consts: monomorphic;
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);
wenzelm [Fri, 21 Oct 2005 18:14:44 +0200] rev 17964
renamed triv_goal to goalI, rev_triv_goal to goalD;
removed mk_triv_goal (cf. Goal.init);
wenzelm [Fri, 21 Oct 2005 18:14:43 +0200] rev 17963
added goal.ML;
moved use of goals.ML;
wenzelm [Fri, 21 Oct 2005 18:14:42 +0200] rev 17962
added goal.ML;
wenzelm [Fri, 21 Oct 2005 18:14:41 +0200] rev 17961
Goal.norm_hhf_rule, Goal.init;
wenzelm [Fri, 21 Oct 2005 18:14:40 +0200] rev 17960
avoid triv_goal and home-grown meta_allE;
wenzelm [Fri, 21 Oct 2005 18:14:38 +0200] rev 17959
OldGoals;
wenzelm [Fri, 21 Oct 2005 18:14:37 +0200] rev 17958
proper header;
proper use of ML files;
wenzelm [Fri, 21 Oct 2005 18:14:36 +0200] rev 17957
avoid home-grown meta_allE;
wenzelm [Fri, 21 Oct 2005 18:14:34 +0200] rev 17956
Goal.prove;
wenzelm [Fri, 21 Oct 2005 18:14:32 +0200] rev 17955
avoid shortcuts from OldGoals;
wenzelm [Fri, 21 Oct 2005 16:34:22 +0200] rev 17954
added simplified settings for Poly/ML 4.x (commented out);
wenzelm [Fri, 21 Oct 2005 16:22:59 +0200] rev 17953
reverted (accidental?) change of 1.148;
haftmann [Fri, 21 Oct 2005 14:49:49 +0200] rev 17952
abandoned rational number functions in favor of General/rat.ML
haftmann [Fri, 21 Oct 2005 14:49:04 +0200] rev 17951
introduced functions from Pure/General/rat.ML
haftmann [Fri, 21 Oct 2005 14:47:37 +0200] rev 17950
slight corrections
haftmann [Fri, 21 Oct 2005 10:32:59 +0200] rev 17949
substantially improved integration of website into distribution framework
haftmann [Fri, 21 Oct 2005 10:32:04 +0200] rev 17948
substantially improved integration of website into distribution framework
haftmann [Fri, 21 Oct 2005 10:27:02 +0200] rev 17947
substantially improved integration of website into distribution framework
haftmann [Fri, 21 Oct 2005 10:21:38 +0200] rev 17946
substantially improved integration of website into distribution framework
haftmann [Fri, 21 Oct 2005 09:54:03 +0200] rev 17945
towards an improved website/makedist integration
haftmann [Fri, 21 Oct 2005 09:18:27 +0200] rev 17944
towards an improved website/makedist integration
haftmann [Fri, 21 Oct 2005 09:08:42 +0200] rev 17943
added default distinfo.mak
haftmann [Fri, 21 Oct 2005 09:05:52 +0200] rev 17942
towards an improved website/makedist integration
haftmann [Fri, 21 Oct 2005 09:05:52 +0200] rev 17941
towards an improved website/makedist integration
haftmann [Fri, 21 Oct 2005 08:23:45 +0200] rev 17940
added rounding functions
mengj [Fri, 21 Oct 2005 02:57:22 +0200] rev 17939
Merged theory ResAtpOracle.thy into ResAtpMethods.thy