Sat, 16 Oct 2010 17:10:23 -0700 |
huffman |
remove dead code
|
file |
diff |
annotate
|
Sat, 16 Oct 2010 16:22:42 -0700 |
huffman |
remove last few dependencies on domain_library.ML and delete it; temporarily disable emptiness check
|
file |
diff |
annotate
|
Sat, 16 Oct 2010 15:26:30 -0700 |
huffman |
reimplement proof automation for coinduct rules
|
file |
diff |
annotate
|
Fri, 15 Oct 2010 08:52:53 -0700 |
huffman |
move emptiness check to comp_theorems; remove eqs parameter to prove_induction; remove dead code
|
file |
diff |
annotate
|
Fri, 15 Oct 2010 08:07:20 -0700 |
huffman |
simplify automation of induct proof
|
file |
diff |
annotate
|
Fri, 15 Oct 2010 05:50:27 -0700 |
huffman |
rewrite proof automation for finite_ind; get rid of case_UU_tac
|
file |
diff |
annotate
|
Thu, 14 Oct 2010 19:16:52 -0700 |
huffman |
put constructor argument specs in constr_info type
|
file |
diff |
annotate
|
Thu, 14 Oct 2010 14:42:05 -0700 |
huffman |
avoid using Global_Theory.get_thm
|
file |
diff |
annotate
|
Thu, 14 Oct 2010 13:46:27 -0700 |
huffman |
include iso_info as part of constr_info type
|
file |
diff |
annotate
|
Thu, 14 Oct 2010 13:28:31 -0700 |
huffman |
remove function Domain_Theorems.theorems; bind theorem names directly from Domain_Constructors.add_domain_constructors
|
file |
diff |
annotate
|
Thu, 14 Oct 2010 09:44:40 -0700 |
huffman |
add record type synonym 'constr_info'
|
file |
diff |
annotate
|
Thu, 14 Oct 2010 09:34:00 -0700 |
huffman |
add function take_theorems
|
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
|
Sun, 12 Sep 2010 19:04:02 +0200 |
wenzelm |
eliminated aliases of Type.constraint;
|
file |
diff |
annotate
|
Thu, 10 Jun 2010 12:24:03 +0200 |
haftmann |
tuned quotes, antiquotations and whitespace
|
file |
diff |
annotate
|
Thu, 27 May 2010 17:41:27 +0200 |
wenzelm |
renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
|
file |
diff |
annotate
|
Mon, 24 May 2010 11:29:49 -0700 |
huffman |
move unused pattern match syntax stuff into HOLCF/ex
|
file |
diff |
annotate
|
Sat, 22 May 2010 13:27:36 -0700 |
huffman |
removed fixrec_simp attribute (cf. a2a1c8a658ef)
|
file |
diff |
annotate
|
Tue, 11 May 2010 12:38:07 -0700 |
huffman |
simplify code for emptiness check
|
file |
diff |
annotate
|
Wed, 05 May 2010 18:25:34 +0200 |
haftmann |
farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
|
file |
diff |
annotate
|
Mon, 03 May 2010 14:25:56 +0200 |
wenzelm |
renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
|
file |
diff |
annotate
|
Thu, 15 Apr 2010 18:21:05 -0700 |
huffman |
add rule deflation_ID to proof script for take + constructor rules
|
file |
diff |
annotate
|
Mon, 15 Mar 2010 21:57:35 +0100 |
wenzelm |
moved old Sign.intern_term to the place where it is still used;
|
file |
diff |
annotate
|
Sat, 13 Mar 2010 21:07:20 -0800 |
huffman |
add case name 'adm' for infinite induction rules
|
file |
diff |
annotate
|
Sat, 13 Mar 2010 20:15:25 -0800 |
huffman |
renamed some lemmas generated by the domain package
|
file |
diff |
annotate
|
Sat, 13 Mar 2010 17:05:34 -0800 |
huffman |
pass binding as argument to add_domain_constructors; proper binding for case combinator
|
file |
diff |
annotate
|
Sat, 13 Mar 2010 16:48:57 -0800 |
huffman |
pass domain binding as argument to Domain_Theorems.theorems; proper qualified bindings for theorem names
|
file |
diff |
annotate
|
Sat, 13 Mar 2010 15:51:12 -0800 |
huffman |
pass take_info as argument to Domain_Theorems.theorems
|
file |
diff |
annotate
|
Sat, 13 Mar 2010 15:18:25 -0800 |
huffman |
replace some string arguments with bindings
|
file |
diff |
annotate
|
Mon, 08 Mar 2010 14:42:40 -0800 |
huffman |
remove unnecessary error handling code
|
file |
diff |
annotate
|
Mon, 08 Mar 2010 14:12:51 -0800 |
huffman |
construct fully typed goal in proof of induction rule
|
file |
diff |
annotate
|
Mon, 08 Mar 2010 13:58:00 -0800 |
huffman |
don't generate rule foo.finites for non-flat domains; use take_induct rule to prove induction rule
|
file |
diff |
annotate
|
Mon, 08 Mar 2010 12:43:44 -0800 |
huffman |
remove redundant function arguments
|
file |
diff |
annotate
|
Mon, 08 Mar 2010 12:36:26 -0800 |
huffman |
include take_info within take_induct_info type
|
file |
diff |
annotate
|
Mon, 08 Mar 2010 12:21:07 -0800 |
huffman |
pass take_info as an argument to comp_theorems
|
file |
diff |
annotate
|
Mon, 08 Mar 2010 11:58:40 -0800 |
huffman |
pass take_induct_info as an argument to comp_theorems
|
file |
diff |
annotate
|
Mon, 08 Mar 2010 09:37:03 -0800 |
huffman |
move proofs of reach and take lemmas to domain_take_proofs.ML
|
file |
diff |
annotate
|
Sun, 07 Mar 2010 16:39:31 -0800 |
huffman |
generate separate qualified theorem name for each type's reach and take_lemma
|
file |
diff |
annotate
|
Sat, 06 Mar 2010 16:02:22 -0800 |
huffman |
add case_names attribute to casedist and ind rules
|
file |
diff |
annotate
|
Fri, 05 Mar 2010 15:59:48 -0800 |
huffman |
print message when finiteness of domain definition is detected
|
file |
diff |
annotate
|
Fri, 05 Mar 2010 15:25:59 -0800 |
huffman |
skip coinduction proofs for indirect-recursive domain definitions
|
file |
diff |
annotate
|
Fri, 05 Mar 2010 14:50:37 -0800 |
huffman |
introduce notion of 'decisive' deflations; use them to simplify proof script for rule 'finites'
|
file |
diff |
annotate
|
Fri, 05 Mar 2010 13:33:17 -0800 |
huffman |
fix proof script so 'domain foo = Foo foo' works
|
file |
diff |
annotate
|
Fri, 05 Mar 2010 09:09:11 -0800 |
huffman |
skip proof of induction rule for indirect-recursive domain definitions
|
file |
diff |
annotate
|
Thu, 04 Mar 2010 10:01:39 -0800 |
huffman |
move coinduction-related stuff into function prove_coindunction
|
file |
diff |
annotate
|
Wed, 03 Mar 2010 08:20:20 -0800 |
huffman |
remove unnecessary theorem references
|
file |
diff |
annotate
|
Wed, 03 Mar 2010 08:14:56 -0800 |
huffman |
remove copy_of_dtyp from domain_axioms.ML
|
file |
diff |
annotate
|
Wed, 03 Mar 2010 07:55:52 -0800 |
huffman |
add_axioms returns an iso_info; add_theorems takes an iso_info as an argument
|
file |
diff |
annotate
|
Wed, 03 Mar 2010 07:36:31 -0800 |
huffman |
uniformly use variable names m and n in take-related lemmas; use export_without_context where appropriate
|
file |
diff |
annotate
|
Tue, 02 Mar 2010 19:45:37 -0800 |
huffman |
proof scripts use variable name y for casedist
|
file |
diff |
annotate
|
Tue, 02 Mar 2010 16:25:59 -0800 |
huffman |
fix proof script for take_apps so it works with indirect recursion
|
file |
diff |
annotate
|
Tue, 02 Mar 2010 15:53:07 -0800 |
huffman |
remove unused mixfix component from type cons
|
file |
diff |
annotate
|
Tue, 02 Mar 2010 13:50:23 -0800 |
huffman |
move take-related definitions and proofs to new module; simplify map_of_typ functions
|
file |
diff |
annotate
|
Tue, 02 Mar 2010 09:54:50 -0800 |
huffman |
remove dead code
|
file |
diff |
annotate
|
Tue, 02 Mar 2010 04:31:50 -0800 |
huffman |
re-enable bisim code, now in domain_theorems.ML
|
file |
diff |
annotate
|
Tue, 02 Mar 2010 00:34:26 -0800 |
huffman |
domain package no longer generates copy functions; all proofs use take functions instead
|
file |
diff |
annotate
|
Mon, 01 Mar 2010 09:55:32 -0800 |
huffman |
move definition of case combinator to domain_constructors.ML
|
file |
diff |
annotate
|
Mon, 01 Mar 2010 07:35:14 -0800 |
huffman |
move proofs of pat_rews to domain_constructors.ML
|
file |
diff |
annotate
|
Sun, 28 Feb 2010 20:56:28 -0800 |
huffman |
add_domain_constructors takes iso_info record as argument
|
file |
diff |
annotate
|
Sun, 28 Feb 2010 08:55:01 -0800 |
huffman |
move definition and syntax of pattern combinators into domain_constructors.ML
|
file |
diff |
annotate
|