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);