| Fri, 29 Oct 2010 17:15:28 -0700 |
huffman |
renamed {Rep,Abs}_CFun to {Rep,Abs}_cfun
|
file |
diff |
annotate
|
| Sat, 23 Oct 2010 11:04:26 -0700 |
huffman |
change fixrec parser to not accept theorem names with (unchecked) option
|
file |
diff |
annotate
|
| Tue, 19 Oct 2010 16:21:24 -0700 |
huffman |
replace fixrec 'permissive' mode with per-equation 'unchecked' option
|
file |
diff |
annotate
|
| Tue, 19 Oct 2010 07:05:04 -0700 |
huffman |
simplify fixrec pattern match function
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 13:26:21 -0700 |
huffman |
remove code for obsolete 'fixpat' command
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 12:54:17 -0700 |
huffman |
clean up definition of compile_pat function
|
file |
diff |
annotate
|
| Wed, 15 Sep 2010 10:34:39 -0700 |
huffman |
rename some fixrec pattern-match compilation functions
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 16:05:25 +0200 |
wenzelm |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
|
file |
diff |
annotate
|
| Mon, 24 May 2010 09:32:52 -0700 |
huffman |
rename type 'a maybe to 'a match; rename Fixrec.return to Fixrec.succeed
|
file |
diff |
annotate
|
| Sat, 22 May 2010 18:34:38 -0700 |
huffman |
for functions with only variable patterns, fixrec definitions no longer use Fixrec.return/Fixrec.run
|
file |
diff |
annotate
|
| Sat, 22 May 2010 17:57:16 -0700 |
huffman |
simplify fixrec continuity tactic
|
file |
diff |
annotate
|
| 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
|