Wed, 31 Oct 2001 22:00:02 +0100 global statements: locale argument;
wenzelm [Wed, 31 Oct 2001 22:00:02 +0100] rev 12006
global statements: locale argument;
Wed, 31 Oct 2001 21:59:25 +0100 added local_standard;
wenzelm [Wed, 31 Oct 2001 21:59:25 +0100] rev 12005
added local_standard;
Wed, 31 Oct 2001 21:59:07 +0100 IsarThy.theorem_i: no locale;
wenzelm [Wed, 31 Oct 2001 21:59:07 +0100] rev 12004
IsarThy.theorem_i: no locale;
Wed, 31 Oct 2001 21:58:04 +0100 removed obsolete (rule equal_intr_rule);
wenzelm [Wed, 31 Oct 2001 21:58:04 +0100] rev 12003
removed obsolete (rule equal_intr_rule);
Wed, 31 Oct 2001 20:00:35 +0100 Additional rules for simplifying inside "Goal"
berghofe [Wed, 31 Oct 2001 20:00:35 +0100] rev 12002
Additional rules for simplifying inside "Goal"
Wed, 31 Oct 2001 19:59:21 +0100 - Tuned add_cnstrt
berghofe [Wed, 31 Oct 2001 19:59:21 +0100] rev 12001
- Tuned add_cnstrt - Fixed bug in reconstruct_proof that caused infinite loop
Wed, 31 Oct 2001 19:49:36 +0100 Removed name_thm from finish_global.
berghofe [Wed, 31 Oct 2001 19:49:36 +0100] rev 12000
Removed name_thm from finish_global.
Wed, 31 Oct 2001 19:41:29 +0100 Tuned function thm_proof.
berghofe [Wed, 31 Oct 2001 19:41:29 +0100] rev 11999
Tuned function thm_proof.
Wed, 31 Oct 2001 19:37:04 +0100 - enter_thmx -> enter_thms
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
Wed, 31 Oct 2001 19:32:05 +0100 norm_hhf_eq is now stored using open_store_standard_thm.
berghofe [Wed, 31 Oct 2001 19:32:05 +0100] rev 11997
norm_hhf_eq is now stored using open_store_standard_thm.
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip