wenzelm [Sun, 04 Nov 2001 20:56:19 +0100] rev 12042
updated;
berghofe [Sat, 03 Nov 2001 18:49:40 +0100] rev 12041
Fixed bug in function add_npvars.
wenzelm [Sat, 03 Nov 2001 18:44:49 +0100] rev 12040
updated;
wenzelm [Sat, 03 Nov 2001 18:42:55 +0100] rev 12039
tuned;
wenzelm [Sat, 03 Nov 2001 18:42:38 +0100] rev 12038
proper use of bind_thm(s);
wenzelm [Sat, 03 Nov 2001 18:42:00 +0100] rev 12037
adapted to new-style theories;
wenzelm [Sat, 03 Nov 2001 18:41:28 +0100] rev 12036
GPLed;
wenzelm [Sat, 03 Nov 2001 18:41:13 +0100] rev 12035
converted theory Dnat;
wenzelm [Sat, 03 Nov 2001 18:40:21 +0100] rev 12034
* 'domain' package adapted to new-style theories, e.g. see
HOLCF/ex/Dnat.thy;
wenzelm [Sat, 03 Nov 2001 01:45:32 +0100] rev 12033
document setup;
wenzelm [Sat, 03 Nov 2001 01:44:45 +0100] rev 12032
replaced Undef by UU;
wenzelm [Sat, 03 Nov 2001 01:44:26 +0100] rev 12031
ax_flat;
wenzelm [Sat, 03 Nov 2001 01:41:26 +0100] rev 12030
GPLed;
wenzelm [Sat, 03 Nov 2001 01:40:28 +0100] rev 12029
tuned;
wenzelm [Sat, 03 Nov 2001 01:39:17 +0100] rev 12028
replaced Undef by UU;
wenzelm [Sat, 03 Nov 2001 01:38:39 +0100] rev 12027
converted theory Lift;
wenzelm [Sat, 03 Nov 2001 01:38:11 +0100] rev 12026
rep_datatype lift;
converted to new-style theory;
wenzelm [Sat, 03 Nov 2001 01:36:19 +0100] rev 12025
moved into Main;
wenzelm [Sat, 03 Nov 2001 01:35:11 +0100] rev 12024
moved String into Main;
wenzelm [Sat, 03 Nov 2001 01:33:54 +0100] rev 12023
tuned;
wenzelm [Sat, 03 Nov 2001 01:33:33 +0100] rev 12022
HOLCF: proper rep_datatype lift (see theory Lift); use plain induct_tac
instead of lift.induct_tac, use UU instead of Undef in cases;
wenzelm [Fri, 02 Nov 2001 22:02:41 +0100] rev 12021
declare transitive;
wenzelm [Fri, 02 Nov 2001 22:01:58 +0100] rev 12020
theory Calculation move to Set;
wenzelm [Fri, 02 Nov 2001 22:01:07 +0100] rev 12019
transitive declared in Pure;
paulson [Fri, 02 Nov 2001 17:55:24 +0100] rev 12018
Numerals and simprocs for types real and hypreal. The abstract
constants 0, 1 and binary numerals work harmoniously.
wenzelm [Thu, 01 Nov 2001 21:12:13 +0100] rev 12017
Goals.add_locale;
wenzelm [Thu, 01 Nov 2001 21:11:52 +0100] rev 12016
fix_frees;
improved export_def: handle args on lhs;
wenzelm [Thu, 01 Nov 2001 21:11:17 +0100] rev 12015
theorem: locale argument;
wenzelm [Thu, 01 Nov 2001 21:10:47 +0100] rev 12014
beginnings of new locales (not yet functional);
wenzelm [Thu, 01 Nov 2001 21:10:13 +0100] rev 12013
Goals.setup;
wenzelm [Thu, 01 Nov 2001 21:09:53 +0100] rev 12012
parking code for old-style locales here;
wenzelm [Wed, 31 Oct 2001 22:05:37 +0100] rev 12011
tuned notation (degree instead of dollar);
wenzelm [Wed, 31 Oct 2001 22:04:29 +0100] rev 12010
theorem(_i): locale argument;
contexts 0 and 1 in state now refer to theory and locale, respectively;
unified export (no longer uses global "standard");
wenzelm [Wed, 31 Oct 2001 22:02:33 +0100] rev 12009
Proof.init_state thy None;
wenzelm [Wed, 31 Oct 2001 22:02:11 +0100] rev 12008
simplified export;
tuned printing of fixes;
wenzelm [Wed, 31 Oct 2001 22:00:25 +0100] rev 12007
'atomize': CHANGED_PROP;
wenzelm [Wed, 31 Oct 2001 22:00:02 +0100] rev 12006
global statements: locale argument;
wenzelm [Wed, 31 Oct 2001 21:59:25 +0100] rev 12005
added local_standard;
wenzelm [Wed, 31 Oct 2001 21:59:07 +0100] rev 12004
IsarThy.theorem_i: no locale;
wenzelm [Wed, 31 Oct 2001 21:58:04 +0100] rev 12003
removed obsolete (rule equal_intr_rule);
berghofe [Wed, 31 Oct 2001 20:00:35 +0100] rev 12002
Additional rules for simplifying inside "Goal"
berghofe [Wed, 31 Oct 2001 19:59:21 +0100] rev 12001
- Tuned add_cnstrt
- Fixed bug in reconstruct_proof that caused infinite loop
berghofe [Wed, 31 Oct 2001 19:49:36 +0100] rev 12000
Removed name_thm from finish_global.
berghofe [Wed, 31 Oct 2001 19:41:29 +0100] rev 11999
Tuned function thm_proof.
berghofe [Wed, 31 Oct 2001 19:37:04 +0100] rev 11998
- enter_thmx -> enter_thms
- improved naming of theorems: enter_thms now takes functions pre_name and post_name
as arguments
berghofe [Wed, 31 Oct 2001 19:32:05 +0100] rev 11997
norm_hhf_eq is now stored using open_store_standard_thm.
wenzelm [Wed, 31 Oct 2001 01:28:39 +0100] rev 11996
induct: internalize ``missing'' consumes-facts from goal state
(enables unstructured scripts to perform elim-style induction);
wenzelm [Wed, 31 Oct 2001 01:27:04 +0100] rev 11995
- 'induct' may now use elim-style induction rules without chaining
facts, using ``missing'' premises from the goal state; this allows
rules stemming from inductive sets to be applied in unstructured
scripts, while still benefitting from proper handling of non-atomic
statements; NB: major inductive premises need to be put first, all the
rest of the goal is passed through the induction;