diff options
| author | Josh Chen | 2020-07-31 14:56:24 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-07-31 14:56:24 +0200 |
| commit | ff5454812f9e2720bd90c3a5437505644f63b487 (patch) | |
| tree | 2df5f45de006c56391118db75e2f185036b02cd7 /spartan/core/goals.ML | |
| parent | 2b0e14b16dcef0e829da95800b3c0af1975bb1ce (diff) | |
(FEAT) Term elaboration of assumption and goal statements.
. spartan/core/goals.ML
. spartan/core/elaboration.ML
. spartan/core/elaborated_statement.ML
(FEAT) More context tacticals and search tacticals.
. spartan/core/context_tactical.ML
(FEAT) Improved subgoal focus.
Moves fully elaborated assumptions into the context (MINOR INCOMPATIBILITY).
. spartan/core/focus.ML
(FIX) Normalize facts in order to be able to resolve properly.
. spartan/core/typechecking.ML
(MAIN) New definitions.
(MAIN) Renamed theories and theorems.
(MAIN) Refactor theories to fit new features.
Diffstat (limited to '')
| -rw-r--r-- | spartan/core/goals.ML | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/spartan/core/goals.ML b/spartan/core/goals.ML index 87ec2b8..540f5c7 100644 --- a/spartan/core/goals.ML +++ b/spartan/core/goals.ML @@ -1,9 +1,9 @@ (* Title: goals.ML - Author: Makarius Wenzel, Joshua Chen + Author: Joshua Chen Goal statements and proof term export. -Modified from code originally written by Makarius Wenzel. +Modified from code contained in ~~/Pure/Isar/specification.ML. *) local @@ -184,15 +184,15 @@ val schematic_theorem_cmd = gen_schematic_theorem Bundle.includes_cmd Attrib.check_src - Elaborated_Assumption.read_goal_statement + Elaborated_Statement.read_goal_statement fun theorem spec descr = Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr) - ( Scan.option (Args.parens (Args.$$$ "derive")) + ( Scan.option (Args.parens (Args.$$$ "def")) -- (long_statement || short_statement) >> (fn (opt_derive, (long, binding, includes, elems, concl)) => schematic_theorem_cmd - (case opt_derive of SOME "derive" => true | _ => false) + (case opt_derive of SOME "def" => true | _ => false) long descr NONE (K I) binding includes elems concl) ) fun definition spec descr = |