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
wenzelm [Wed, 19 Oct 2005 21:53:34 +0200] rev 17938
obsolete;
wenzelm [Wed, 19 Oct 2005 21:52:50 +0200] rev 17937
removed add_inductive_x;
wenzelm [Wed, 19 Oct 2005 21:52:49 +0200] rev 17936
removed obsolete add_datatype_x;
tuned;
wenzelm [Wed, 19 Oct 2005 21:52:48 +0200] rev 17935
removed obsolete thy_syntax.ML;
wenzelm [Wed, 19 Oct 2005 21:52:47 +0200] rev 17934
removed obsolete old_symbol_source;
wenzelm [Wed, 19 Oct 2005 21:52:46 +0200] rev 17933
removed obsolete non-Isar theory format and old Isar theory headers;
wenzelm [Wed, 19 Oct 2005 21:52:45 +0200] rev 17932
removed old-style theory format;
tuned;
wenzelm [Wed, 19 Oct 2005 21:52:44 +0200] rev 17931
avoid lagacy read function;
wenzelm [Wed, 19 Oct 2005 21:52:43 +0200] rev 17930
added thm(s) retrieval functions (from goals.ML);
wenzelm [Wed, 19 Oct 2005 21:52:42 +0200] rev 17929
removed obsolete old-locales;
moved thm(s) retrieval functions back to pure_thy.ML;
removed atomic_goal(w) interface;
removed user-level (top_sg, prin, printyp, pprint_term/typ, which tend to cause some confusion about the implicit goal (!) context being used here;