1995-03-07 Moved declarations of @QSUM and <*> to a syntax section.
lcp [Tue, 07 Mar 1995 13:18:48 +0100] rev 929
Moved declarations of @QSUM and <*> to a syntax section. Changed print_translation because <*> is now an infix.
1995-03-07 Moved declaration of ~= to a syntax section
lcp [Tue, 07 Mar 1995 13:15:25 +0100] rev 928
Moved declaration of ~= to a syntax section
1995-03-03 replaced Pure by ProtoPure
clasohm [Fri, 03 Mar 1995 12:48:06 +0100] rev 927
replaced Pure by ProtoPure
1995-03-03 fixed a bug in infer_types/exn_type_msg
clasohm [Fri, 03 Mar 1995 12:34:57 +0100] rev 926
fixed a bug in infer_types/exn_type_msg
1995-03-03 new version of HOL/Integ with curried function application
clasohm [Fri, 03 Mar 1995 12:04:45 +0100] rev 925
new version of HOL/Integ with curried function application
1995-03-03 new version of HOL/IMP with curried function application
clasohm [Fri, 03 Mar 1995 12:04:16 +0100] rev 924
new version of HOL/IMP with curried function application
1995-03-03 new version of HOL with curried function application
clasohm [Fri, 03 Mar 1995 12:02:25 +0100] rev 923
new version of HOL with curried function application
1995-03-03 added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
clasohm [Fri, 03 Mar 1995 11:48:05 +0100] rev 922
added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
1995-03-02 added declaration of syntactic const "_abs";
wenzelm [Thu, 02 Mar 1995 12:07:20 +0100] rev 921
added declaration of syntactic const "_abs";
1995-02-28 Added initial /bin/csh line and comments
lcp [Tue, 28 Feb 1995 10:54:49 +0100] rev 920
Added initial /bin/csh line and comments
1995-02-28 No longer calls maketest; instead, the Makefile writes the file
lcp [Tue, 28 Feb 1995 10:53:56 +0100] rev 919
No longer calls maketest; instead, the Makefile writes the file test.
1995-02-28 Uses "suffix substitution" to shorten macro definitions.
lcp [Tue, 28 Feb 1995 10:51:52 +0100] rev 918
Uses "suffix substitution" to shorten macro definitions.
1995-02-28 Re-organised to perform the tests independently. Now test
lcp [Tue, 28 Feb 1995 10:50:37 +0100] rev 917
Re-organised to perform the tests independently. Now test is defined in terms of separate targets IMP, ex, etc. If ISABELLECOMP is set wrongly then "exit 1" causes the Make to fail. Defines the macro "LOGIC" to refer to the right command for running the object-logic. Uses "suffix substitution" to shorten macro definitions.
1995-02-28 New example by Jacob Frost, tidied by lcp
lcp [Tue, 28 Feb 1995 10:33:52 +0100] rev 916
New example by Jacob Frost, tidied by lcp
1995-02-27 New example by Jacob Frost, tidied by lcp
lcp [Mon, 27 Feb 1995 18:12:21 +0100] rev 915
New example by Jacob Frost, tidied by lcp
1995-02-27 Now prove_goalw_cterm calls print_sign_exn_unit, so that the rest
lcp [Mon, 27 Feb 1995 18:07:59 +0100] rev 914
Now prove_goalw_cterm calls print_sign_exn_unit, so that the rest of the error message ("The exception above was raised for...") will appear. And print_exn calls print_sign_exn_unit so that it can re-raise the SAME exception.
1995-02-27 Updated the "version" variable (which was never done for
lcp [Mon, 27 Feb 1995 18:05:38 +0100] rev 913
Updated the "version" variable (which was never done for Isabelle-94 revisions 1 and 2!)
1995-02-27 Redefined functions to suppress redundant leading 0s and 1s
lcp [Mon, 27 Feb 1995 17:51:12 +0100] rev 912
Redefined functions to suppress redundant leading 0s and 1s
1995-02-27 new in mixfix annotations: "' " (quote space) separates delimiters without
wenzelm [Mon, 27 Feb 1995 17:47:57 +0100] rev 911
new in mixfix annotations: "' " (quote space) separates delimiters without adding extra white space for printing;
1995-02-27 Added the exception handler
lcp [Mon, 27 Feb 1995 17:47:44 +0100] rev 910
Added the exception handler handle _ => exit 1. This will catch all errors and force an exit with error code, causing Make to fail.
1995-02-27 intro_tacsf now includes subsetI as an introduction rule. It is
lcp [Mon, 27 Feb 1995 17:44:43 +0100] rev 909
intro_tacsf now includes subsetI as an introduction rule. It is needed for rules like list_into_univ
1995-02-27 Updated comment about list_subset_univ and list_into_univ.
lcp [Mon, 27 Feb 1995 17:40:57 +0100] rev 908
Updated comment about list_subset_univ and list_into_univ.
1995-02-27 exit: new, for use in Makefiles
lcp [Mon, 27 Feb 1995 17:27:50 +0100] rev 907
exit: new, for use in Makefiles
1995-02-27 Redefined arithmetic to suppress redundant leading 0s and 1s
lcp [Mon, 27 Feb 1995 17:11:25 +0100] rev 906
Redefined arithmetic to suppress redundant leading 0s and 1s renamed the infix 2239 to the constant Bcons, as numerals eliminate the need for the infix.
1995-02-27 Added integer numerals (mostly due to Markus Wenzel)
lcp [Mon, 27 Feb 1995 17:08:51 +0100] rev 905
Added integer numerals (mostly due to Markus Wenzel) renamed the infix 2239 to the constant Bcons, as numerals eliminate the need for the infix.
1995-02-27 Proved zadd_left_commute and zmult_left_commute to define
lcp [Mon, 27 Feb 1995 17:06:19 +0100] rev 904
Proved zadd_left_commute and zmult_left_commute to define zadd_ac and zmult_ac. Deleted add_cong, add_kill and add_left_commute_kill as unused. Defined zadd_simps, zminus_simps, zmult_simps and added them to integ_ss.
1995-02-27 New shell script for finding orphan .ML files (those with no
lcp [Mon, 27 Feb 1995 16:58:59 +0100] rev 903
New shell script for finding orphan .ML files (those with no .thy file)
1995-02-24 added ExcludeThm; cleaned up Makefile; fixed isalpha bug (replaced by isalnum)
clasohm [Fri, 24 Feb 1995 11:52:19 +0100] rev 902
added ExcludeThm; cleaned up Makefile; fixed isalpha bug (replaced by isalnum)
1995-02-17 added check "length ts > 1" before printing ambiguity warning in infer_types
clasohm [Fri, 17 Feb 1995 13:25:11 +0100] rev 901
added check "length ts > 1" before printing ambiguity warning in infer_types
1995-02-16 Improved test for looping rewrite rules.
nipkow [Thu, 16 Feb 1995 08:55:15 +0100] rev 900
Improved test for looping rewrite rules.
1995-02-15 replaced pair_ss by prod_ss
regensbu [Wed, 15 Feb 1995 20:02:47 +0100] rev 899
replaced pair_ss by prod_ss
1995-02-08 Improved check for looping conditional rewrite rules.
nipkow [Wed, 08 Feb 1995 11:30:00 +0100] rev 898
Improved check for looping conditional rewrite rules.
1995-02-07 ID for the file
regensbu [Tue, 07 Feb 1995 17:36:48 +0100] rev 897
ID for the file
1995-02-07 ID for the file
regensbu [Tue, 07 Feb 1995 17:35:49 +0100] rev 896
ID for the file
1995-02-07 'get ID update working'
regensbu [Tue, 07 Feb 1995 17:30:34 +0100] rev 895
'get ID update working'
1995-02-07 CVS:
regensbu [Tue, 07 Feb 1995 17:26:32 +0100] rev 894
CVS: CVS:
1995-02-07 CVS:
regensbu [Tue, 07 Feb 1995 17:25:31 +0100] rev 893
CVS:
1995-02-07 added qed, qed_goal[w]
clasohm [Tue, 07 Feb 1995 11:59:32 +0100] rev 892
added qed, qed_goal[w]
1995-02-03 added specification of csh as script interpreter
clasohm [Fri, 03 Feb 1995 12:32:14 +0100] rev 891
added specification of csh as script interpreter
1995-02-02 simplified elimination of chain productions
clasohm [Thu, 02 Feb 1995 13:11:51 +0100] rev 890
simplified elimination of chain productions
1995-01-27 binder: optional body pri now [bracketted];
wenzelm [Fri, 27 Jan 1995 13:40:07 +0100] rev 889
binder: optional body pri now [bracketted];
1995-01-27 improved read_xrules: patterns no longer read twice;
wenzelm [Fri, 27 Jan 1995 13:35:29 +0100] rev 888
improved read_xrules: patterns no longer read twice; tuned read_typ;
1995-01-27 *** empty log message ***
wenzelm [Fri, 27 Jan 1995 13:33:52 +0100] rev 887
*** empty log message ***
1995-01-27 instance: now automatically includes defs of current thy node as witnesses;
wenzelm [Fri, 27 Jan 1995 13:31:26 +0100] rev 886
instance: now automatically includes defs of current thy node as witnesses;
1995-01-27 binder: optional body pri now [bracketted];
wenzelm [Fri, 27 Jan 1995 13:29:44 +0100] rev 885
binder: optional body pri now [bracketted];
1995-01-27 added documentation of pwd
clasohm [Fri, 27 Jan 1995 12:42:03 +0100] rev 884
added documentation of pwd
1995-01-27 renamed Sign.ambiguity_level to Syntax.ambiguity_level
clasohm [Fri, 27 Jan 1995 12:31:18 +0100] rev 883
renamed Sign.ambiguity_level to Syntax.ambiguity_level
1995-01-27 moved ambiguity_level from sign.ML to Syntax/syntax.ML
clasohm [Fri, 27 Jan 1995 12:30:36 +0100] rev 882
moved ambiguity_level from sign.ML to Syntax/syntax.ML
(0) -300 -100 -48 +48 +100 +300 +1000 +3000 +10000 +30000 tip