Sat, 22 May 2010 14:04:05 -0700 |
huffman |
optimize continuity proofs in fixrec package, using cont2cont rules
|
file |
diff |
annotate
|
Sat, 22 May 2010 12:56:33 -0700 |
huffman |
simplify definition of eta_tac
|
file |
diff |
annotate
|
Sat, 22 May 2010 12:36:50 -0700 |
huffman |
remove fixrec_simp attribute; fixrec uses default simpset from theory context instead
|
file |
diff |
annotate
|
Sat, 22 May 2010 10:02:07 -0700 |
huffman |
remove cont2cont simproc; instead declare cont2cont rules as simp rules
|
file |
diff |
annotate
|
Wed, 19 May 2010 13:07:15 -0700 |
huffman |
more informative error message for fixrec when continuity proof fails
|
file |
diff |
annotate
|
Mon, 17 May 2010 23:54:15 +0200 |
wenzelm |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file |
diff |
annotate
|
Sun, 16 May 2010 00:02:11 +0200 |
wenzelm |
prefer structure Parse_Spec;
|
file |
diff |
annotate
|
Wed, 12 May 2010 15:25:58 +0200 |
wenzelm |
updated/unified some legacy warnings;
|
file |
diff |
annotate
|
Sat, 01 May 2010 07:53:42 -0700 |
huffman |
fixrec no longer uses global simpset internally to prove equations
|
file |
diff |
annotate
|
Mon, 22 Mar 2010 14:44:37 -0700 |
huffman |
fix ML warnings in fixrec.ML
|
file |
diff |
annotate
|
Sat, 13 Mar 2010 19:06:18 -0800 |
huffman |
use Simplifier.context to avoid 'no proof context in simpset' errors from fixrec_simp after theory merge
|
file |
diff |
annotate
|
Sat, 13 Mar 2010 18:16:48 -0800 |
huffman |
fixpat command prints legacy_feature warning
|
file |
diff |
annotate
|
Sat, 13 Mar 2010 14:26:26 -0800 |
huffman |
avoid unnecessary primed variable names
|
file |
diff |
annotate
|
Sat, 13 Mar 2010 10:38:38 -0800 |
huffman |
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy
|
file |
diff |
annotate
|
Sat, 13 Mar 2010 10:00:45 -0800 |
huffman |
fixrec now generates qualified theorem names
|
file |
diff |
annotate
|
Sun, 07 Mar 2010 11:57:16 +0100 |
wenzelm |
modernized structure Local_Defs;
|
file |
diff |
annotate
|
Tue, 02 Mar 2010 18:16:28 -0800 |
huffman |
fixrec and repdef modules import holcf_library
|
file |
diff |
annotate
|
Tue, 02 Mar 2010 17:21:10 -0800 |
huffman |
proper names for types cfun, sprod, ssum
|
file |
diff |
annotate
|
Thu, 19 Nov 2009 14:46:33 +0100 |
wenzelm |
adapted Local_Theory.define -- eliminated odd thm kind;
|
file |
diff |
annotate
|
Tue, 17 Nov 2009 14:51:57 +0100 |
wenzelm |
eliminated slightly odd name space grouping -- now managed by Isar toplevel;
|
file |
diff |
annotate
|
Fri, 13 Nov 2009 21:11:15 +0100 |
wenzelm |
modernized structure Local_Theory;
|
file |
diff |
annotate
|
Fri, 13 Nov 2009 20:41:29 +0100 |
wenzelm |
eliminated slightly odd kind argument of LocalTheory.note(s);
|
file |
diff |
annotate
|
Fri, 13 Nov 2009 17:25:09 +0100 |
wenzelm |
eliminated obsolete "generated" kind -- collapsed to unspecific "" (definitely unused according to Lukas Bulwahn);
|
file |
diff |
annotate
|
Sun, 08 Nov 2009 18:43:42 +0100 |
wenzelm |
adapted Theory_Data;
|
file |
diff |
annotate
|
Sun, 08 Nov 2009 16:30:41 +0100 |
wenzelm |
adapted Generic_Data, Proof_Data;
|
file |
diff |
annotate
|
Sat, 07 Nov 2009 07:37:20 -0800 |
huffman |
merged
|
file |
diff |
annotate
|
Thu, 05 Nov 2009 15:38:09 -0800 |
huffman |
use try instead of handle
|
file |
diff |
annotate
|
Thu, 05 Nov 2009 17:02:43 +0100 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
Tue, 03 Nov 2009 19:01:06 -0800 |
huffman |
better error handling for fixrec_simp
|
file |
diff |
annotate
|
Tue, 03 Nov 2009 18:32:30 -0800 |
huffman |
domain package registers fixrec_simp lemmas
|
file |
diff |
annotate
|
Tue, 03 Nov 2009 17:03:21 -0800 |
huffman |
add fixrec_simp attribute and method (eventually to replace fixpat)
|
file |
diff |
annotate
|
Mon, 02 Nov 2009 18:39:41 -0800 |
huffman |
add fixrec support for HOL pair constructor patterns
|
file |
diff |
annotate
|
Mon, 19 Oct 2009 23:02:56 +0200 |
wenzelm |
always qualify NJ's old List.foldl/foldr in Isabelle/ML;
|
file |
diff |
annotate
|
Thu, 15 Oct 2009 23:28:10 +0200 |
wenzelm |
replaced String.concat by implode;
|
file |
diff |
annotate
|
Thu, 23 Jul 2009 18:44:09 +0200 |
wenzelm |
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
|
file |
diff |
annotate
|
Sun, 21 Jun 2009 15:45:57 +0200 |
haftmann |
discontinued ancient tradition to suffix certain ML module names with "_package"
|
file |
diff |
annotate
| base
|