diff options
| author | Josh Chen | 2020-07-28 14:10:34 +0200 |
|---|---|---|
| committer | Josh Chen | 2020-07-28 14:10:34 +0200 |
| commit | 6b27aa578257a6f4db9242b413a8008962b7f2e1 (patch) | |
| tree | f49e1decc18bddb4a2ccbc4b181d470eac77ed03 /spartan/core/goals.ML | |
| parent | 223a253732ced7d89dcea506ab56d92d1cfe8281 (diff) | |
New `assuming` proof command for elaborated assumptions
Diffstat (limited to 'spartan/core/goals.ML')
| -rw-r--r-- | spartan/core/goals.ML | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/spartan/core/goals.ML b/spartan/core/goals.ML index 3e2bd09..87ec2b8 100644 --- a/spartan/core/goals.ML +++ b/spartan/core/goals.ML @@ -184,7 +184,7 @@ val schematic_theorem_cmd = gen_schematic_theorem Bundle.includes_cmd Attrib.check_src - Elaborated_Expression.read_statement + Elaborated_Assumption.read_goal_statement fun theorem spec descr = Outer_Syntax.local_theory_to_proof' spec ("state " ^ descr) |